(set-info :smt-lib-version 2.6)
(set-logic QF_BV)
(set-info :source |
Search for 15368 FLOP solution to size-512 FFT
Steve Haynal <steve@softerhardware.com>
|)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun Wbase_64_0_64 () (_ BitVec 7))
(declare-fun Wbase_64_4_64 () (_ BitVec 7))
(declare-fun Wbase_64_8_64 () (_ BitVec 7))
(declare-fun Wbase_64_12_64 () (_ BitVec 7))
(declare-fun Wbase_64_16_64 () (_ BitVec 7))
(declare-fun Wbase_64_20_64 () (_ BitVec 7))
(declare-fun Wbase_64_24_64 () (_ BitVec 7))
(declare-fun Wbase_64_28_64 () (_ BitVec 7))
(declare-fun Wbase_64_32_64 () (_ BitVec 7))
(declare-fun Wbase_64_36_64 () (_ BitVec 7))
(declare-fun Wbase_64_40_64 () (_ BitVec 7))
(declare-fun Wbase_64_44_64 () (_ BitVec 7))
(declare-fun Wbase_64_48_64 () (_ BitVec 7))
(declare-fun Wbase_64_52_64 () (_ BitVec 7))
(declare-fun Wbase_64_56_64 () (_ BitVec 7))
(declare-fun Wbase_64_60_64 () (_ BitVec 7))
(declare-fun Wbase_32_0_32 () (_ BitVec 7))
(declare-fun Wbase_32_4_32 () (_ BitVec 7))
(declare-fun Wbase_32_8_32 () (_ BitVec 7))
(declare-fun Wbase_32_12_32 () (_ BitVec 7))
(declare-fun Wbase_32_16_32 () (_ BitVec 7))
(declare-fun Wbase_32_20_32 () (_ BitVec 7))
(declare-fun Wbase_32_24_32 () (_ BitVec 7))
(declare-fun Wbase_32_28_32 () (_ BitVec 7))
(declare-fun Wbase_32_0_160 () (_ BitVec 7))
(declare-fun Wbase_32_4_160 () (_ BitVec 7))
(declare-fun Wbase_32_8_160 () (_ BitVec 7))
(declare-fun Wbase_32_12_160 () (_ BitVec 7))
(declare-fun Wbase_32_16_160 () (_ BitVec 7))
(declare-fun Wbase_32_20_160 () (_ BitVec 7))
(declare-fun Wbase_32_24_160 () (_ BitVec 7))
(declare-fun Wbase_32_28_160 () (_ BitVec 7))
(declare-fun Wbase_16_0_16 () (_ BitVec 7))
(declare-fun Wbase_16_4_16 () (_ BitVec 7))
(declare-fun Wbase_16_8_16 () (_ BitVec 7))
(declare-fun Wbase_16_12_16 () (_ BitVec 7))
(declare-fun Wbase_16_0_144 () (_ BitVec 7))
(declare-fun Wbase_16_4_144 () (_ BitVec 7))
(declare-fun Wbase_16_8_144 () (_ BitVec 7))
(declare-fun Wbase_16_12_144 () (_ BitVec 7))
(declare-fun Wbase_16_0_80 () (_ BitVec 7))
(declare-fun Wbase_16_4_80 () (_ BitVec 7))
(declare-fun Wbase_16_8_80 () (_ BitVec 7))
(declare-fun Wbase_16_12_80 () (_ BitVec 7))
(declare-fun Wbase_16_0_208 () (_ BitVec 7))
(declare-fun Wbase_16_4_208 () (_ BitVec 7))
(declare-fun Wbase_16_8_208 () (_ BitVec 7))
(declare-fun Wbase_16_12_208 () (_ BitVec 7))
(declare-fun Wbase_8_0_8 () (_ BitVec 7))
(declare-fun Wbase_8_4_8 () (_ BitVec 7))
(declare-fun Wbase_8_0_136 () (_ BitVec 7))
(declare-fun Wbase_8_4_136 () (_ BitVec 7))
(declare-fun Wbase_8_0_72 () (_ BitVec 7))
(declare-fun Wbase_8_4_72 () (_ BitVec 7))
(declare-fun Wbase_8_0_200 () (_ BitVec 7))
(declare-fun Wbase_8_4_200 () (_ BitVec 7))
(declare-fun Wbase_8_0_40 () (_ BitVec 7))
(declare-fun Wbase_8_4_40 () (_ BitVec 7))
(declare-fun Wbase_8_0_168 () (_ BitVec 7))
(declare-fun Wbase_8_4_168 () (_ BitVec 7))
(declare-fun Wbase_8_0_104 () (_ BitVec 7))
(declare-fun Wbase_8_4_104 () (_ BitVec 7))
(declare-fun Wbase_8_0_232 () (_ BitVec 7))
(declare-fun Wbase_8_4_232 () (_ BitVec 7))
(declare-fun Wbase_4_0_4 () (_ BitVec 7))
(declare-fun Wbase_4_0_132 () (_ BitVec 7))
(declare-fun Wbase_4_0_68 () (_ BitVec 7))
(declare-fun Wbase_4_0_196 () (_ BitVec 7))
(declare-fun Wbase_4_0_36 () (_ BitVec 7))
(declare-fun Wbase_4_0_164 () (_ BitVec 7))
(declare-fun Wbase_4_0_100 () (_ BitVec 7))
(declare-fun Wbase_4_0_228 () (_ BitVec 7))
(declare-fun Wbase_4_0_20 () (_ BitVec 7))
(declare-fun Wbase_4_0_148 () (_ BitVec 7))
(declare-fun Wbase_4_0_84 () (_ BitVec 7))
(declare-fun Wbase_4_0_212 () (_ BitVec 7))
(declare-fun Wbase_4_0_52 () (_ BitVec 7))
(declare-fun Wbase_4_0_180 () (_ BitVec 7))
(declare-fun Wbase_4_0_116 () (_ BitVec 7))
(declare-fun Wbase_4_0_244 () (_ BitVec 7))
(assert
(let ((?Wbase_128_0_128 (_ bv0 7)))
(let ((?Wbase_128_4_128 (_ bv0 7)))
(let ((?Wbase_128_8_128 (_ bv0 7)))
(let ((?Wbase_128_12_128 (_ bv0 7)))
(let ((?Wbase_128_16_128 (_ bv0 7)))
(let ((?Wbase_128_20_128 (_ bv0 7)))
(let ((?Wbase_128_24_128 (_ bv0 7)))
(let ((?Wbase_128_28_128 (_ bv0 7)))
(let ((?Wbase_128_32_128 (_ bv0 7)))
(let ((?Wbase_128_36_128 (_ bv0 7)))
(let ((?Wbase_128_40_128 (_ bv0 7)))
(let ((?Wbase_128_44_128 (_ bv0 7)))
(let ((?Wbase_128_48_128 (_ bv0 7)))
(let ((?Wbase_128_52_128 (_ bv0 7)))
(let ((?Wbase_128_56_128 (_ bv0 7)))
(let ((?Wbase_128_60_128 (_ bv0 7)))
(let ((?Wbase_128_64_128 (_ bv0 7)))
(let ((?Wbase_128_68_128 (_ bv0 7)))
(let ((?Wbase_128_72_128 (_ bv0 7)))
(let ((?Wbase_128_76_128 (_ bv0 7)))
(let ((?Wbase_128_80_128 (_ bv0 7)))
(let ((?Wbase_128_84_128 (_ bv0 7)))
(let ((?Wbase_128_88_128 (_ bv0 7)))
(let ((?Wbase_128_92_128 (_ bv0 7)))
(let ((?Wbase_128_96_128 (_ bv0 7)))
(let ((?Wbase_128_100_128 (_ bv0 7)))
(let ((?Wbase_128_104_128 (_ bv0 7)))
(let ((?Wbase_128_108_128 (_ bv0 7)))
(let ((?Wbase_128_112_128 (_ bv0 7)))
(let ((?Wbase_128_116_128 (_ bv0 7)))
(let ((?Wbase_128_120_128 (_ bv0 7)))
(let ((?Wbase_128_124_128 (_ bv0 7)))
(let ((?rWbase_64_0_64 (bvadd Wbase_64_0_64 (_ bv64 7))))
(let ((?Wbase_64_0_320 Wbase_64_0_64))
(let ((?rWbase_64_4_64 (bvadd Wbase_64_4_64 (_ bv64 7))))
(let ((?Wbase_64_4_320 Wbase_64_4_64))
(let ((?rWbase_64_8_64 (bvadd Wbase_64_8_64 (_ bv64 7))))
(let ((?Wbase_64_8_320 Wbase_64_8_64))
(let ((?rWbase_64_12_64 (bvadd Wbase_64_12_64 (_ bv64 7))))
(let ((?Wbase_64_12_320 Wbase_64_12_64))
(let ((?rWbase_64_16_64 (bvadd Wbase_64_16_64 (_ bv64 7))))
(let ((?Wbase_64_16_320 Wbase_64_16_64))
(let ((?rWbase_64_20_64 (bvadd Wbase_64_20_64 (_ bv64 7))))
(let ((?Wbase_64_20_320 Wbase_64_20_64))
(let ((?rWbase_64_24_64 (bvadd Wbase_64_24_64 (_ bv64 7))))
(let ((?Wbase_64_24_320 Wbase_64_24_64))
(let ((?rWbase_64_28_64 (bvadd Wbase_64_28_64 (_ bv64 7))))
(let ((?Wbase_64_28_320 Wbase_64_28_64))
(let ((?rWbase_64_32_64 (bvadd Wbase_64_32_64 (_ bv64 7))))
(let ((?Wbase_64_32_320 Wbase_64_32_64))
(let ((?rWbase_64_36_64 (bvadd Wbase_64_36_64 (_ bv64 7))))
(let ((?Wbase_64_36_320 Wbase_64_36_64))
(let ((?rWbase_64_40_64 (bvadd Wbase_64_40_64 (_ bv64 7))))
(let ((?Wbase_64_40_320 Wbase_64_40_64))
(let ((?rWbase_64_44_64 (bvadd Wbase_64_44_64 (_ bv64 7))))
(let ((?Wbase_64_44_320 Wbase_64_44_64))
(let ((?rWbase_64_48_64 (bvadd Wbase_64_48_64 (_ bv64 7))))
(let ((?Wbase_64_48_320 Wbase_64_48_64))
(let ((?rWbase_64_52_64 (bvadd Wbase_64_52_64 (_ bv64 7))))
(let ((?Wbase_64_52_320 Wbase_64_52_64))
(let ((?rWbase_64_56_64 (bvadd Wbase_64_56_64 (_ bv64 7))))
(let ((?Wbase_64_56_320 Wbase_64_56_64))
(let ((?rWbase_64_60_64 (bvadd Wbase_64_60_64 (_ bv64 7))))
(let ((?Wbase_64_60_320 Wbase_64_60_64))
(let ((?rWbase_32_0_32 (bvadd Wbase_32_0_32 (_ bv32 7))))
(let ((?Wbase_32_0_288 Wbase_32_0_32))
(let ((?rWbase_32_4_32 (bvadd Wbase_32_4_32 (_ bv32 7))))
(let ((?Wbase_32_4_288 Wbase_32_4_32))
(let ((?rWbase_32_8_32 (bvadd Wbase_32_8_32 (_ bv32 7))))
(let ((?Wbase_32_8_288 Wbase_32_8_32))
(let ((?rWbase_32_12_32 (bvadd Wbase_32_12_32 (_ bv32 7))))
(let ((?Wbase_32_12_288 Wbase_32_12_32))
(let ((?rWbase_32_16_32 (bvadd Wbase_32_16_32 (_ bv32 7))))
(let ((?Wbase_32_16_288 Wbase_32_16_32))
(let ((?rWbase_32_20_32 (bvadd Wbase_32_20_32 (_ bv32 7))))
(let ((?Wbase_32_20_288 Wbase_32_20_32))
(let ((?rWbase_32_24_32 (bvadd Wbase_32_24_32 (_ bv32 7))))
(let ((?Wbase_32_24_288 Wbase_32_24_32))
(let ((?rWbase_32_28_32 (bvadd Wbase_32_28_32 (_ bv32 7))))
(let ((?Wbase_32_28_288 Wbase_32_28_32))
(let ((?rWbase_32_0_160 (bvadd Wbase_32_0_160 (_ bv32 7))))
(let ((?Wbase_32_0_416 Wbase_32_0_160))
(let ((?rWbase_32_4_160 (bvadd Wbase_32_4_160 (_ bv32 7))))
(let ((?Wbase_32_4_416 Wbase_32_4_160))
(let ((?rWbase_32_8_160 (bvadd Wbase_32_8_160 (_ bv32 7))))
(let ((?Wbase_32_8_416 Wbase_32_8_160))
(let ((?rWbase_32_12_160 (bvadd Wbase_32_12_160 (_ bv32 7))))
(let ((?Wbase_32_12_416 Wbase_32_12_160))
(let ((?rWbase_32_16_160 (bvadd Wbase_32_16_160 (_ bv32 7))))
(let ((?Wbase_32_16_416 Wbase_32_16_160))
(let ((?rWbase_32_20_160 (bvadd Wbase_32_20_160 (_ bv32 7))))
(let ((?Wbase_32_20_416 Wbase_32_20_160))
(let ((?rWbase_32_24_160 (bvadd Wbase_32_24_160 (_ bv32 7))))
(let ((?Wbase_32_24_416 Wbase_32_24_160))
(let ((?rWbase_32_28_160 (bvadd Wbase_32_28_160 (_ bv32 7))))
(let ((?Wbase_32_28_416 Wbase_32_28_160))
(let ((?rWbase_16_0_16 (bvadd Wbase_16_0_16 (_ bv16 7))))
(let ((?Wbase_16_0_272 Wbase_16_0_16))
(let ((?rWbase_16_4_16 (bvadd Wbase_16_4_16 (_ bv16 7))))
(let ((?Wbase_16_4_272 Wbase_16_4_16))
(let ((?rWbase_16_8_16 (bvadd Wbase_16_8_16 (_ bv16 7))))
(let ((?Wbase_16_8_272 Wbase_16_8_16))
(let ((?rWbase_16_12_16 (bvadd Wbase_16_12_16 (_ bv16 7))))
(let ((?Wbase_16_12_272 Wbase_16_12_16))
(let ((?rWbase_16_0_144 (bvadd Wbase_16_0_144 (_ bv16 7))))
(let ((?Wbase_16_0_400 Wbase_16_0_144))
(let ((?rWbase_16_4_144 (bvadd Wbase_16_4_144 (_ bv16 7))))
(let ((?Wbase_16_4_400 Wbase_16_4_144))
(let ((?rWbase_16_8_144 (bvadd Wbase_16_8_144 (_ bv16 7))))
(let ((?Wbase_16_8_400 Wbase_16_8_144))
(let ((?rWbase_16_12_144 (bvadd Wbase_16_12_144 (_ bv16 7))))
(let ((?Wbase_16_12_400 Wbase_16_12_144))
(let ((?rWbase_16_0_80 (bvadd Wbase_16_0_80 (_ bv80 7))))
(let ((?Wbase_16_0_336 Wbase_16_0_80))
(let ((?rWbase_16_4_80 (bvadd Wbase_16_4_80 (_ bv80 7))))
(let ((?Wbase_16_4_336 Wbase_16_4_80))
(let ((?rWbase_16_8_80 (bvadd Wbase_16_8_80 (_ bv80 7))))
(let ((?Wbase_16_8_336 Wbase_16_8_80))
(let ((?rWbase_16_12_80 (bvadd Wbase_16_12_80 (_ bv80 7))))
(let ((?Wbase_16_12_336 Wbase_16_12_80))
(let ((?rWbase_16_0_208 (bvadd Wbase_16_0_208 (_ bv80 7))))
(let ((?Wbase_16_0_464 Wbase_16_0_208))
(let ((?rWbase_16_4_208 (bvadd Wbase_16_4_208 (_ bv80 7))))
(let ((?Wbase_16_4_464 Wbase_16_4_208))
(let ((?rWbase_16_8_208 (bvadd Wbase_16_8_208 (_ bv80 7))))
(let ((?Wbase_16_8_464 Wbase_16_8_208))
(let ((?rWbase_16_12_208 (bvadd Wbase_16_12_208 (_ bv80 7))))
(let ((?Wbase_16_12_464 Wbase_16_12_208))
(let ((?rWbase_8_0_8 (bvadd Wbase_8_0_8 (_ bv8 7))))
(let ((?Wbase_8_0_264 Wbase_8_0_8))
(let ((?rWbase_8_4_8 (bvadd Wbase_8_4_8 (_ bv8 7))))
(let ((?Wbase_8_4_264 Wbase_8_4_8))
(let ((?rWbase_8_0_136 (bvadd Wbase_8_0_136 (_ bv8 7))))
(let ((?Wbase_8_0_392 Wbase_8_0_136))
(let ((?rWbase_8_4_136 (bvadd Wbase_8_4_136 (_ bv8 7))))
(let ((?Wbase_8_4_392 Wbase_8_4_136))
(let ((?rWbase_8_0_72 (bvadd Wbase_8_0_72 (_ bv72 7))))
(let ((?Wbase_8_0_328 Wbase_8_0_72))
(let ((?rWbase_8_4_72 (bvadd Wbase_8_4_72 (_ bv72 7))))
(let ((?Wbase_8_4_328 Wbase_8_4_72))
(let ((?rWbase_8_0_200 (bvadd Wbase_8_0_200 (_ bv72 7))))
(let ((?Wbase_8_0_456 Wbase_8_0_200))
(let ((?rWbase_8_4_200 (bvadd Wbase_8_4_200 (_ bv72 7))))
(let ((?Wbase_8_4_456 Wbase_8_4_200))
(let ((?rWbase_8_0_40 (bvadd Wbase_8_0_40 (_ bv40 7))))
(let ((?Wbase_8_0_296 Wbase_8_0_40))
(let ((?rWbase_8_4_40 (bvadd Wbase_8_4_40 (_ bv40 7))))
(let ((?Wbase_8_4_296 Wbase_8_4_40))
(let ((?rWbase_8_0_168 (bvadd Wbase_8_0_168 (_ bv40 7))))
(let ((?Wbase_8_0_424 Wbase_8_0_168))
(let ((?rWbase_8_4_168 (bvadd Wbase_8_4_168 (_ bv40 7))))
(let ((?Wbase_8_4_424 Wbase_8_4_168))
(let ((?rWbase_8_0_104 (bvadd Wbase_8_0_104 (_ bv104 7))))
(let ((?Wbase_8_0_360 Wbase_8_0_104))
(let ((?rWbase_8_4_104 (bvadd Wbase_8_4_104 (_ bv104 7))))
(let ((?Wbase_8_4_360 Wbase_8_4_104))
(let ((?rWbase_8_0_232 (bvadd Wbase_8_0_232 (_ bv104 7))))
(let ((?Wbase_8_0_488 Wbase_8_0_232))
(let ((?rWbase_8_4_232 (bvadd Wbase_8_4_232 (_ bv104 7))))
(let ((?Wbase_8_4_488 Wbase_8_4_232))
(let ((?rWbase_4_0_4 (bvadd Wbase_4_0_4 (_ bv4 7))))
(let ((?Wbase_4_0_260 Wbase_4_0_4))
(let ((?rWbase_4_0_132 (bvadd Wbase_4_0_132 (_ bv4 7))))
(let ((?Wbase_4_0_388 Wbase_4_0_132))
(let ((?rWbase_4_0_68 (bvadd Wbase_4_0_68 (_ bv68 7))))
(let ((?Wbase_4_0_324 Wbase_4_0_68))
(let ((?rWbase_4_0_196 (bvadd Wbase_4_0_196 (_ bv68 7))))
(let ((?Wbase_4_0_452 Wbase_4_0_196))
(let ((?rWbase_4_0_36 (bvadd Wbase_4_0_36 (_ bv36 7))))
(let ((?Wbase_4_0_292 Wbase_4_0_36))
(let ((?rWbase_4_0_164 (bvadd Wbase_4_0_164 (_ bv36 7))))
(let ((?Wbase_4_0_420 Wbase_4_0_164))
(let ((?rWbase_4_0_100 (bvadd Wbase_4_0_100 (_ bv100 7))))
(let ((?Wbase_4_0_356 Wbase_4_0_100))
(let ((?rWbase_4_0_228 (bvadd Wbase_4_0_228 (_ bv100 7))))
(let ((?Wbase_4_0_484 Wbase_4_0_228))
(let ((?rWbase_4_0_20 (bvadd Wbase_4_0_20 (_ bv20 7))))
(let ((?Wbase_4_0_276 Wbase_4_0_20))
(let ((?rWbase_4_0_148 (bvadd Wbase_4_0_148 (_ bv20 7))))
(let ((?Wbase_4_0_404 Wbase_4_0_148))
(let ((?rWbase_4_0_84 (bvadd Wbase_4_0_84 (_ bv84 7))))
(let ((?Wbase_4_0_340 Wbase_4_0_84))
(let ((?rWbase_4_0_212 (bvadd Wbase_4_0_212 (_ bv84 7))))
(let ((?Wbase_4_0_468 Wbase_4_0_212))
(let ((?rWbase_4_0_52 (bvadd Wbase_4_0_52 (_ bv52 7))))
(let ((?Wbase_4_0_308 Wbase_4_0_52))
(let ((?rWbase_4_0_180 (bvadd Wbase_4_0_180 (_ bv52 7))))
(let ((?Wbase_4_0_436 Wbase_4_0_180))
(let ((?rWbase_4_0_116 (bvadd Wbase_4_0_116 (_ bv116 7))))
(let ((?Wbase_4_0_372 Wbase_4_0_116))
(let ((?rWbase_4_0_244 (bvadd Wbase_4_0_244 (_ bv116 7))))
(let ((?Wbase_4_0_500 Wbase_4_0_244))
(let ((?ltfp_128_0_128 (bvsub Wbase_64_0_64 ?Wbase_128_0_128)))
(let ((?ltfp_128_4_128 (bvsub Wbase_64_4_64 ?Wbase_128_4_128)))
(let ((?ltfp_128_8_128 (bvsub Wbase_64_8_64 ?Wbase_128_8_128)))
(let ((?ltfp_128_12_128 (bvsub Wbase_64_12_64 ?Wbase_128_12_128)))
(let ((?ltfp_128_16_128 (bvsub Wbase_64_16_64 ?Wbase_128_16_128)))
(let ((?ltfp_128_20_128 (bvsub Wbase_64_20_64 ?Wbase_128_20_128)))
(let ((?ltfp_128_24_128 (bvsub Wbase_64_24_64 ?Wbase_128_24_128)))
(let ((?ltfp_128_28_128 (bvsub Wbase_64_28_64 ?Wbase_128_28_128)))
(let ((?ltfp_128_32_128 (bvsub Wbase_64_32_64 ?Wbase_128_32_128)))
(let ((?ltfp_128_36_128 (bvsub Wbase_64_36_64 ?Wbase_128_36_128)))
(let ((?ltfp_128_40_128 (bvsub Wbase_64_40_64 ?Wbase_128_40_128)))
(let ((?ltfp_128_44_128 (bvsub Wbase_64_44_64 ?Wbase_128_44_128)))
(let ((?ltfp_128_48_128 (bvsub Wbase_64_48_64 ?Wbase_128_48_128)))
(let ((?ltfp_128_52_128 (bvsub Wbase_64_52_64 ?Wbase_128_52_128)))
(let ((?ltfp_128_56_128 (bvsub Wbase_64_56_64 ?Wbase_128_56_128)))
(let ((?ltfp_128_60_128 (bvsub Wbase_64_60_64 ?Wbase_128_60_128)))
(let ((?ltfp_128_64_128 (bvsub ?rWbase_64_0_64 ?Wbase_128_64_128)))
(let ((?ltfp_128_68_128 (bvsub ?rWbase_64_4_64 ?Wbase_128_68_128)))
(let ((?ltfp_128_72_128 (bvsub ?rWbase_64_8_64 ?Wbase_128_72_128)))
(let ((?ltfp_128_76_128 (bvsub ?rWbase_64_12_64 ?Wbase_128_76_128)))
(let ((?ltfp_128_80_128 (bvsub ?rWbase_64_16_64 ?Wbase_128_80_128)))
(let ((?ltfp_128_84_128 (bvsub ?rWbase_64_20_64 ?Wbase_128_84_128)))
(let ((?ltfp_128_88_128 (bvsub ?rWbase_64_24_64 ?Wbase_128_88_128)))
(let ((?ltfp_128_92_128 (bvsub ?rWbase_64_28_64 ?Wbase_128_92_128)))
(let ((?ltfp_128_96_128 (bvsub ?rWbase_64_32_64 ?Wbase_128_96_128)))
(let ((?ltfp_128_100_128 (bvsub ?rWbase_64_36_64 ?Wbase_128_100_128)))
(let ((?ltfp_128_104_128 (bvsub ?rWbase_64_40_64 ?Wbase_128_104_128)))
(let ((?ltfp_128_108_128 (bvsub ?rWbase_64_44_64 ?Wbase_128_108_128)))
(let ((?ltfp_128_112_128 (bvsub ?rWbase_64_48_64 ?Wbase_128_112_128)))
(let ((?ltfp_128_116_128 (bvsub ?rWbase_64_52_64 ?Wbase_128_116_128)))
(let ((?ltfp_128_120_128 (bvsub ?rWbase_64_56_64 ?Wbase_128_120_128)))
(let ((?ltfp_128_124_128 (bvsub ?rWbase_64_60_64 ?Wbase_128_124_128)))
(let ((?ltfp_64_0_64 (bvsub Wbase_32_0_32 Wbase_64_0_64)))
(let ((?ltfp_64_4_64 (bvsub Wbase_32_4_32 Wbase_64_4_64)))
(let ((?ltfp_64_8_64 (bvsub Wbase_32_8_32 Wbase_64_8_64)))
(let ((?ltfp_64_12_64 (bvsub Wbase_32_12_32 Wbase_64_12_64)))
(let ((?ltfp_64_16_64 (bvsub Wbase_32_16_32 Wbase_64_16_64)))
(let ((?ltfp_64_20_64 (bvsub Wbase_32_20_32 Wbase_64_20_64)))
(let ((?ltfp_64_24_64 (bvsub Wbase_32_24_32 Wbase_64_24_64)))
(let ((?ltfp_64_28_64 (bvsub Wbase_32_28_32 Wbase_64_28_64)))
(let ((?ltfp_64_32_64 (bvsub ?rWbase_32_0_32 Wbase_64_32_64)))
(let ((?ltfp_64_36_64 (bvsub ?rWbase_32_4_32 Wbase_64_36_64)))
(let ((?ltfp_64_40_64 (bvsub ?rWbase_32_8_32 Wbase_64_40_64)))
(let ((?ltfp_64_44_64 (bvsub ?rWbase_32_12_32 Wbase_64_44_64)))
(let ((?ltfp_64_48_64 (bvsub ?rWbase_32_16_32 Wbase_64_48_64)))
(let ((?ltfp_64_52_64 (bvsub ?rWbase_32_20_32 Wbase_64_52_64)))
(let ((?ltfp_64_56_64 (bvsub ?rWbase_32_24_32 Wbase_64_56_64)))
(let ((?ltfp_64_60_64 (bvsub ?rWbase_32_28_32 Wbase_64_60_64)))
(let ((?ltfp_64_0_320 (bvsub Wbase_32_0_160 ?Wbase_64_0_320)))
(let ((?ltfp_64_4_320 (bvsub Wbase_32_4_160 ?Wbase_64_4_320)))
(let ((?ltfp_64_8_320 (bvsub Wbase_32_8_160 ?Wbase_64_8_320)))
(let ((?ltfp_64_12_320 (bvsub Wbase_32_12_160 ?Wbase_64_12_320)))
(let ((?ltfp_64_16_320 (bvsub Wbase_32_16_160 ?Wbase_64_16_320)))
(let ((?ltfp_64_20_320 (bvsub Wbase_32_20_160 ?Wbase_64_20_320)))
(let ((?ltfp_64_24_320 (bvsub Wbase_32_24_160 ?Wbase_64_24_320)))
(let ((?ltfp_64_28_320 (bvsub Wbase_32_28_160 ?Wbase_64_28_320)))
(let ((?ltfp_64_32_320 (bvsub ?rWbase_32_0_160 ?Wbase_64_32_320)))
(let ((?ltfp_64_36_320 (bvsub ?rWbase_32_4_160 ?Wbase_64_36_320)))
(let ((?ltfp_64_40_320 (bvsub ?rWbase_32_8_160 ?Wbase_64_40_320)))
(let ((?ltfp_64_44_320 (bvsub ?rWbase_32_12_160 ?Wbase_64_44_320)))
(let ((?ltfp_64_48_320 (bvsub ?rWbase_32_16_160 ?Wbase_64_48_320)))
(let ((?ltfp_64_52_320 (bvsub ?rWbase_32_20_160 ?Wbase_64_52_320)))
(let ((?ltfp_64_56_320 (bvsub ?rWbase_32_24_160 ?Wbase_64_56_320)))
(let ((?ltfp_64_60_320 (bvsub ?rWbase_32_28_160 ?Wbase_64_60_320)))
(let ((?ltfp_32_0_32 (bvsub Wbase_16_0_16 Wbase_32_0_32)))
(let ((?ltfp_32_4_32 (bvsub Wbase_16_4_16 Wbase_32_4_32)))
(let ((?ltfp_32_8_32 (bvsub Wbase_16_8_16 Wbase_32_8_32)))
(let ((?ltfp_32_12_32 (bvsub Wbase_16_12_16 Wbase_32_12_32)))
(let ((?ltfp_32_16_32 (bvsub ?rWbase_16_0_16 Wbase_32_16_32)))
(let ((?ltfp_32_20_32 (bvsub ?rWbase_16_4_16 Wbase_32_20_32)))
(let ((?ltfp_32_24_32 (bvsub ?rWbase_16_8_16 Wbase_32_24_32)))
(let ((?ltfp_32_28_32 (bvsub ?rWbase_16_12_16 Wbase_32_28_32)))
(let ((?ltfp_32_0_288 (bvsub Wbase_16_0_144 ?Wbase_32_0_288)))
(let ((?ltfp_32_4_288 (bvsub Wbase_16_4_144 ?Wbase_32_4_288)))
(let ((?ltfp_32_8_288 (bvsub Wbase_16_8_144 ?Wbase_32_8_288)))
(let ((?ltfp_32_12_288 (bvsub Wbase_16_12_144 ?Wbase_32_12_288)))
(let ((?ltfp_32_16_288 (bvsub ?rWbase_16_0_144 ?Wbase_32_16_288)))
(let ((?ltfp_32_20_288 (bvsub ?rWbase_16_4_144 ?Wbase_32_20_288)))
(let ((?ltfp_32_24_288 (bvsub ?rWbase_16_8_144 ?Wbase_32_24_288)))
(let ((?ltfp_32_28_288 (bvsub ?rWbase_16_12_144 ?Wbase_32_28_288)))
(let ((?ltfp_32_0_160 (bvsub Wbase_16_0_80 Wbase_32_0_160)))
(let ((?ltfp_32_4_160 (bvsub Wbase_16_4_80 Wbase_32_4_160)))
(let ((?ltfp_32_8_160 (bvsub Wbase_16_8_80 Wbase_32_8_160)))
(let ((?ltfp_32_12_160 (bvsub Wbase_16_12_80 Wbase_32_12_160)))
(let ((?ltfp_32_16_160 (bvsub ?rWbase_16_0_80 Wbase_32_16_160)))
(let ((?ltfp_32_20_160 (bvsub ?rWbase_16_4_80 Wbase_32_20_160)))
(let ((?ltfp_32_24_160 (bvsub ?rWbase_16_8_80 Wbase_32_24_160)))
(let ((?ltfp_32_28_160 (bvsub ?rWbase_16_12_80 Wbase_32_28_160)))
(let ((?ltfp_32_0_416 (bvsub Wbase_16_0_208 ?Wbase_32_0_416)))
(let ((?ltfp_32_4_416 (bvsub Wbase_16_4_208 ?Wbase_32_4_416)))
(let ((?ltfp_32_8_416 (bvsub Wbase_16_8_208 ?Wbase_32_8_416)))
(let ((?ltfp_32_12_416 (bvsub Wbase_16_12_208 ?Wbase_32_12_416)))
(let ((?ltfp_32_16_416 (bvsub ?rWbase_16_0_208 ?Wbase_32_16_416)))
(let ((?ltfp_32_20_416 (bvsub ?rWbase_16_4_208 ?Wbase_32_20_416)))
(let ((?ltfp_32_24_416 (bvsub ?rWbase_16_8_208 ?Wbase_32_24_416)))
(let ((?ltfp_32_28_416 (bvsub ?rWbase_16_12_208 ?Wbase_32_28_416)))
(let ((?ltfp_16_0_16 (bvsub Wbase_8_0_8 Wbase_16_0_16)))
(let ((?ltfp_16_4_16 (bvsub Wbase_8_4_8 Wbase_16_4_16)))
(let ((?ltfp_16_8_16 (bvsub ?rWbase_8_0_8 Wbase_16_8_16)))
(let ((?ltfp_16_12_16 (bvsub ?rWbase_8_4_8 Wbase_16_12_16)))
(let ((?ltfp_16_0_272 (bvsub Wbase_8_0_136 ?Wbase_16_0_272)))
(let ((?ltfp_16_4_272 (bvsub Wbase_8_4_136 ?Wbase_16_4_272)))
(let ((?ltfp_16_8_272 (bvsub ?rWbase_8_0_136 ?Wbase_16_8_272)))
(let ((?ltfp_16_12_272 (bvsub ?rWbase_8_4_136 ?Wbase_16_12_272)))
(let ((?ltfp_16_0_144 (bvsub Wbase_8_0_72 Wbase_16_0_144)))
(let ((?ltfp_16_4_144 (bvsub Wbase_8_4_72 Wbase_16_4_144)))
(let ((?ltfp_16_8_144 (bvsub ?rWbase_8_0_72 Wbase_16_8_144)))
(let ((?ltfp_16_12_144 (bvsub ?rWbase_8_4_72 Wbase_16_12_144)))
(let ((?ltfp_16_0_400 (bvsub Wbase_8_0_200 ?Wbase_16_0_400)))
(let ((?ltfp_16_4_400 (bvsub Wbase_8_4_200 ?Wbase_16_4_400)))
(let ((?ltfp_16_8_400 (bvsub ?rWbase_8_0_200 ?Wbase_16_8_400)))
(let ((?ltfp_16_12_400 (bvsub ?rWbase_8_4_200 ?Wbase_16_12_400)))
(let ((?ltfp_16_0_80 (bvsub Wbase_8_0_40 Wbase_16_0_80)))
(let ((?ltfp_16_4_80 (bvsub Wbase_8_4_40 Wbase_16_4_80)))
(let ((?ltfp_16_8_80 (bvsub ?rWbase_8_0_40 Wbase_16_8_80)))
(let ((?ltfp_16_12_80 (bvsub ?rWbase_8_4_40 Wbase_16_12_80)))
(let ((?ltfp_16_0_336 (bvsub Wbase_8_0_168 ?Wbase_16_0_336)))
(let ((?ltfp_16_4_336 (bvsub Wbase_8_4_168 ?Wbase_16_4_336)))
(let ((?ltfp_16_8_336 (bvsub ?rWbase_8_0_168 ?Wbase_16_8_336)))
(let ((?ltfp_16_12_336 (bvsub ?rWbase_8_4_168 ?Wbase_16_12_336)))
(let ((?ltfp_16_0_208 (bvsub Wbase_8_0_104 Wbase_16_0_208)))
(let ((?ltfp_16_4_208 (bvsub Wbase_8_4_104 Wbase_16_4_208)))
(let ((?ltfp_16_8_208 (bvsub ?rWbase_8_0_104 Wbase_16_8_208)))
(let ((?ltfp_16_12_208 (bvsub ?rWbase_8_4_104 Wbase_16_12_208)))
(let ((?ltfp_16_0_464 (bvsub Wbase_8_0_232 ?Wbase_16_0_464)))
(let ((?ltfp_16_4_464 (bvsub Wbase_8_4_232 ?Wbase_16_4_464)))
(let ((?ltfp_16_8_464 (bvsub ?rWbase_8_0_232 ?Wbase_16_8_464)))
(let ((?ltfp_16_12_464 (bvsub ?rWbase_8_4_232 ?Wbase_16_12_464)))
(let ((?ltfp_8_0_8 (bvsub Wbase_4_0_4 Wbase_8_0_8)))
(let ((?ltfp_8_4_8 (bvsub ?rWbase_4_0_4 Wbase_8_4_8)))
(let ((?ltfp_8_0_264 (bvsub Wbase_4_0_132 ?Wbase_8_0_264)))
(let ((?ltfp_8_4_264 (bvsub ?rWbase_4_0_132 ?Wbase_8_4_264)))
(let ((?ltfp_8_0_136 (bvsub Wbase_4_0_68 Wbase_8_0_136)))
(let ((?ltfp_8_4_136 (bvsub ?rWbase_4_0_68 Wbase_8_4_136)))
(let ((?ltfp_8_0_392 (bvsub Wbase_4_0_196 ?Wbase_8_0_392)))
(let ((?ltfp_8_4_392 (bvsub ?rWbase_4_0_196 ?Wbase_8_4_392)))
(let ((?ltfp_8_0_72 (bvsub Wbase_4_0_36 Wbase_8_0_72)))
(let ((?ltfp_8_4_72 (bvsub ?rWbase_4_0_36 Wbase_8_4_72)))
(let ((?ltfp_8_0_328 (bvsub Wbase_4_0_164 ?Wbase_8_0_328)))
(let ((?ltfp_8_4_328 (bvsub ?rWbase_4_0_164 ?Wbase_8_4_328)))
(let ((?ltfp_8_0_200 (bvsub Wbase_4_0_100 Wbase_8_0_200)))
(let ((?ltfp_8_4_200 (bvsub ?rWbase_4_0_100 Wbase_8_4_200)))
(let ((?ltfp_8_0_456 (bvsub Wbase_4_0_228 ?Wbase_8_0_456)))
(let ((?ltfp_8_4_456 (bvsub ?rWbase_4_0_228 ?Wbase_8_4_456)))
(let ((?ltfp_8_0_40 (bvsub Wbase_4_0_20 Wbase_8_0_40)))
(let ((?ltfp_8_4_40 (bvsub ?rWbase_4_0_20 Wbase_8_4_40)))
(let ((?ltfp_8_0_296 (bvsub Wbase_4_0_148 ?Wbase_8_0_296)))
(let ((?ltfp_8_4_296 (bvsub ?rWbase_4_0_148 ?Wbase_8_4_296)))
(let ((?ltfp_8_0_168 (bvsub Wbase_4_0_84 Wbase_8_0_168)))
(let ((?ltfp_8_4_168 (bvsub ?rWbase_4_0_84 Wbase_8_4_168)))
(let ((?ltfp_8_0_424 (bvsub Wbase_4_0_212 ?Wbase_8_0_424)))
(let ((?ltfp_8_4_424 (bvsub ?rWbase_4_0_212 ?Wbase_8_4_424)))
(let ((?ltfp_8_0_104 (bvsub Wbase_4_0_52 Wbase_8_0_104)))
(let ((?ltfp_8_4_104 (bvsub ?rWbase_4_0_52 Wbase_8_4_104)))
(let ((?ltfp_8_0_360 (bvsub Wbase_4_0_180 ?Wbase_8_0_360)))
(let ((?ltfp_8_4_360 (bvsub ?rWbase_4_0_180 ?Wbase_8_4_360)))
(let ((?ltfp_8_0_232 (bvsub Wbase_4_0_116 Wbase_8_0_232)))
(let ((?ltfp_8_4_232 (bvsub ?rWbase_4_0_116 Wbase_8_4_232)))
(let ((?ltfp_8_0_488 (bvsub Wbase_4_0_244 ?Wbase_8_0_488)))
(let ((?ltfp_8_4_488 (bvsub ?rWbase_4_0_244 ?Wbase_8_4_488)))
(let ((?ltfp_4_0_4 (bvsub (_ bv0 7) Wbase_4_0_4)))
(let ((?ltfp_4_0_260 (bvsub (_ bv0 7) ?Wbase_4_0_260)))
(let ((?ltfp_4_0_132 (bvsub (_ bv0 7) Wbase_4_0_132)))
(let ((?ltfp_4_0_388 (bvsub (_ bv0 7) ?Wbase_4_0_388)))
(let ((?ltfp_4_0_68 (bvsub (_ bv0 7) Wbase_4_0_68)))
(let ((?ltfp_4_0_324 (bvsub (_ bv0 7) ?Wbase_4_0_324)))
(let ((?ltfp_4_0_196 (bvsub (_ bv0 7) Wbase_4_0_196)))
(let ((?ltfp_4_0_452 (bvsub (_ bv0 7) ?Wbase_4_0_452)))
(let ((?ltfp_4_0_36 (bvsub (_ bv0 7) Wbase_4_0_36)))
(let ((?ltfp_4_0_292 (bvsub (_ bv0 7) ?Wbase_4_0_292)))
(let ((?ltfp_4_0_164 (bvsub (_ bv0 7) Wbase_4_0_164)))
(let ((?ltfp_4_0_420 (bvsub (_ bv0 7) ?Wbase_4_0_420)))
(let ((?ltfp_4_0_100 (bvsub (_ bv0 7) Wbase_4_0_100)))
(let ((?ltfp_4_0_356 (bvsub (_ bv0 7) ?Wbase_4_0_356)))
(let ((?ltfp_4_0_228 (bvsub (_ bv0 7) Wbase_4_0_228)))
(let ((?ltfp_4_0_484 (bvsub (_ bv0 7) ?Wbase_4_0_484)))
(let ((?ltfp_4_0_20 (bvsub (_ bv0 7) Wbase_4_0_20)))
(let ((?ltfp_4_0_276 (bvsub (_ bv0 7) ?Wbase_4_0_276)))
(let ((?ltfp_4_0_148 (bvsub (_ bv0 7) Wbase_4_0_148)))
(let ((?ltfp_4_0_404 (bvsub (_ bv0 7) ?Wbase_4_0_404)))
(let ((?ltfp_4_0_84 (bvsub (_ bv0 7) Wbase_4_0_84)))
(let ((?ltfp_4_0_340 (bvsub (_ bv0 7) ?Wbase_4_0_340)))
(let ((?ltfp_4_0_212 (bvsub (_ bv0 7) Wbase_4_0_212)))
(let ((?ltfp_4_0_468 (bvsub (_ bv0 7) ?Wbase_4_0_468)))
(let ((?ltfp_4_0_52 (bvsub (_ bv0 7) Wbase_4_0_52)))
(let ((?ltfp_4_0_308 (bvsub (_ bv0 7) ?Wbase_4_0_308)))
(let ((?ltfp_4_0_180 (bvsub (_ bv0 7) Wbase_4_0_180)))
(let ((?ltfp_4_0_436 (bvsub (_ bv0 7) ?Wbase_4_0_436)))
(let ((?ltfp_4_0_116 (bvsub (_ bv0 7) Wbase_4_0_116)))
(let ((?ltfp_4_0_372 (bvsub (_ bv0 7) ?Wbase_4_0_372)))
(let ((?ltfp_4_0_244 (bvsub (_ bv0 7) Wbase_4_0_244)))
(let ((?ltfp_4_0_500 (bvsub (_ bv0 7) ?Wbase_4_0_500)))
(let ((?lz_128_0_128 (= ((_ extract 5 0) ?ltfp_128_0_128) (_ bv0 6))))
(let ((?msbz_128_0_128 (= ((_ extract 6 6) ?ltfp_128_0_128) (_ bv0 1))))
(let ((?c0_128_0_128 (and ?lz_128_0_128 ?msbz_128_0_128)))
(let ((?nc0_128_0_128 (not ?c0_128_0_128)))
(let ((?c6_128_0_128 (not ?lz_128_0_128)))
(let ((?icost_128_0_128 (concat (ite ?nc0_128_0_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_0_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_4_128 (= ((_ extract 5 0) ?ltfp_128_4_128) (_ bv0 6))))
(let ((?msbz_128_4_128 (= ((_ extract 6 6) ?ltfp_128_4_128) (_ bv0 1))))
(let ((?c0_128_4_128 (and ?lz_128_4_128 ?msbz_128_4_128)))
(let ((?nc0_128_4_128 (not ?c0_128_4_128)))
(let ((?c6_128_4_128 (not ?lz_128_4_128)))
(let ((?icost_128_4_128 (concat (ite ?nc0_128_4_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_4_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_8_128 (= ((_ extract 5 0) ?ltfp_128_8_128) (_ bv0 6))))
(let ((?msbz_128_8_128 (= ((_ extract 6 6) ?ltfp_128_8_128) (_ bv0 1))))
(let ((?c0_128_8_128 (and ?lz_128_8_128 ?msbz_128_8_128)))
(let ((?nc0_128_8_128 (not ?c0_128_8_128)))
(let ((?c6_128_8_128 (not ?lz_128_8_128)))
(let ((?icost_128_8_128 (concat (ite ?nc0_128_8_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_8_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_12_128 (= ((_ extract 5 0) ?ltfp_128_12_128) (_ bv0 6))))
(let ((?msbz_128_12_128 (= ((_ extract 6 6) ?ltfp_128_12_128) (_ bv0 1))))
(let ((?c0_128_12_128 (and ?lz_128_12_128 ?msbz_128_12_128)))
(let ((?nc0_128_12_128 (not ?c0_128_12_128)))
(let ((?c6_128_12_128 (not ?lz_128_12_128)))
(let ((?icost_128_12_128 (concat (ite ?nc0_128_12_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_12_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_16_128 (= ((_ extract 5 0) ?ltfp_128_16_128) (_ bv0 6))))
(let ((?msbz_128_16_128 (= ((_ extract 6 6) ?ltfp_128_16_128) (_ bv0 1))))
(let ((?c0_128_16_128 (and ?lz_128_16_128 ?msbz_128_16_128)))
(let ((?nc0_128_16_128 (not ?c0_128_16_128)))
(let ((?c6_128_16_128 (not ?lz_128_16_128)))
(let ((?icost_128_16_128 (concat (ite ?nc0_128_16_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_16_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_20_128 (= ((_ extract 5 0) ?ltfp_128_20_128) (_ bv0 6))))
(let ((?msbz_128_20_128 (= ((_ extract 6 6) ?ltfp_128_20_128) (_ bv0 1))))
(let ((?c0_128_20_128 (and ?lz_128_20_128 ?msbz_128_20_128)))
(let ((?nc0_128_20_128 (not ?c0_128_20_128)))
(let ((?c6_128_20_128 (not ?lz_128_20_128)))
(let ((?icost_128_20_128 (concat (ite ?nc0_128_20_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_20_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_24_128 (= ((_ extract 5 0) ?ltfp_128_24_128) (_ bv0 6))))
(let ((?msbz_128_24_128 (= ((_ extract 6 6) ?ltfp_128_24_128) (_ bv0 1))))
(let ((?c0_128_24_128 (and ?lz_128_24_128 ?msbz_128_24_128)))
(let ((?nc0_128_24_128 (not ?c0_128_24_128)))
(let ((?c6_128_24_128 (not ?lz_128_24_128)))
(let ((?icost_128_24_128 (concat (ite ?nc0_128_24_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_24_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_28_128 (= ((_ extract 5 0) ?ltfp_128_28_128) (_ bv0 6))))
(let ((?msbz_128_28_128 (= ((_ extract 6 6) ?ltfp_128_28_128) (_ bv0 1))))
(let ((?c0_128_28_128 (and ?lz_128_28_128 ?msbz_128_28_128)))
(let ((?nc0_128_28_128 (not ?c0_128_28_128)))
(let ((?c6_128_28_128 (not ?lz_128_28_128)))
(let ((?icost_128_28_128 (concat (ite ?nc0_128_28_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_28_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_32_128 (= ((_ extract 5 0) ?ltfp_128_32_128) (_ bv0 6))))
(let ((?msbz_128_32_128 (= ((_ extract 6 6) ?ltfp_128_32_128) (_ bv0 1))))
(let ((?c0_128_32_128 (and ?lz_128_32_128 ?msbz_128_32_128)))
(let ((?nc0_128_32_128 (not ?c0_128_32_128)))
(let ((?c6_128_32_128 (not ?lz_128_32_128)))
(let ((?icost_128_32_128 (concat (ite ?nc0_128_32_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_32_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_36_128 (= ((_ extract 5 0) ?ltfp_128_36_128) (_ bv0 6))))
(let ((?msbz_128_36_128 (= ((_ extract 6 6) ?ltfp_128_36_128) (_ bv0 1))))
(let ((?c0_128_36_128 (and ?lz_128_36_128 ?msbz_128_36_128)))
(let ((?nc0_128_36_128 (not ?c0_128_36_128)))
(let ((?c6_128_36_128 (not ?lz_128_36_128)))
(let ((?icost_128_36_128 (concat (ite ?nc0_128_36_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_36_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_40_128 (= ((_ extract 5 0) ?ltfp_128_40_128) (_ bv0 6))))
(let ((?msbz_128_40_128 (= ((_ extract 6 6) ?ltfp_128_40_128) (_ bv0 1))))
(let ((?c0_128_40_128 (and ?lz_128_40_128 ?msbz_128_40_128)))
(let ((?nc0_128_40_128 (not ?c0_128_40_128)))
(let ((?c6_128_40_128 (not ?lz_128_40_128)))
(let ((?icost_128_40_128 (concat (ite ?nc0_128_40_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_40_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_44_128 (= ((_ extract 5 0) ?ltfp_128_44_128) (_ bv0 6))))
(let ((?msbz_128_44_128 (= ((_ extract 6 6) ?ltfp_128_44_128) (_ bv0 1))))
(let ((?c0_128_44_128 (and ?lz_128_44_128 ?msbz_128_44_128)))
(let ((?nc0_128_44_128 (not ?c0_128_44_128)))
(let ((?c6_128_44_128 (not ?lz_128_44_128)))
(let ((?icost_128_44_128 (concat (ite ?nc0_128_44_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_44_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_48_128 (= ((_ extract 5 0) ?ltfp_128_48_128) (_ bv0 6))))
(let ((?msbz_128_48_128 (= ((_ extract 6 6) ?ltfp_128_48_128) (_ bv0 1))))
(let ((?c0_128_48_128 (and ?lz_128_48_128 ?msbz_128_48_128)))
(let ((?nc0_128_48_128 (not ?c0_128_48_128)))
(let ((?c6_128_48_128 (not ?lz_128_48_128)))
(let ((?icost_128_48_128 (concat (ite ?nc0_128_48_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_48_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_52_128 (= ((_ extract 5 0) ?ltfp_128_52_128) (_ bv0 6))))
(let ((?msbz_128_52_128 (= ((_ extract 6 6) ?ltfp_128_52_128) (_ bv0 1))))
(let ((?c0_128_52_128 (and ?lz_128_52_128 ?msbz_128_52_128)))
(let ((?nc0_128_52_128 (not ?c0_128_52_128)))
(let ((?c6_128_52_128 (not ?lz_128_52_128)))
(let ((?icost_128_52_128 (concat (ite ?nc0_128_52_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_52_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_56_128 (= ((_ extract 5 0) ?ltfp_128_56_128) (_ bv0 6))))
(let ((?msbz_128_56_128 (= ((_ extract 6 6) ?ltfp_128_56_128) (_ bv0 1))))
(let ((?c0_128_56_128 (and ?lz_128_56_128 ?msbz_128_56_128)))
(let ((?nc0_128_56_128 (not ?c0_128_56_128)))
(let ((?c6_128_56_128 (not ?lz_128_56_128)))
(let ((?icost_128_56_128 (concat (ite ?nc0_128_56_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_56_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_60_128 (= ((_ extract 5 0) ?ltfp_128_60_128) (_ bv0 6))))
(let ((?msbz_128_60_128 (= ((_ extract 6 6) ?ltfp_128_60_128) (_ bv0 1))))
(let ((?c0_128_60_128 (and ?lz_128_60_128 ?msbz_128_60_128)))
(let ((?nc0_128_60_128 (not ?c0_128_60_128)))
(let ((?c6_128_60_128 (not ?lz_128_60_128)))
(let ((?icost_128_60_128 (concat (ite ?nc0_128_60_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_60_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_64_128 (= ((_ extract 5 0) ?ltfp_128_64_128) (_ bv0 6))))
(let ((?msbz_128_64_128 (= ((_ extract 6 6) ?ltfp_128_64_128) (_ bv0 1))))
(let ((?c0_128_64_128 (and ?lz_128_64_128 ?msbz_128_64_128)))
(let ((?nc0_128_64_128 (not ?c0_128_64_128)))
(let ((?c6_128_64_128 (not ?lz_128_64_128)))
(let ((?icost_128_64_128 (concat (ite ?nc0_128_64_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_64_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_68_128 (= ((_ extract 5 0) ?ltfp_128_68_128) (_ bv0 6))))
(let ((?msbz_128_68_128 (= ((_ extract 6 6) ?ltfp_128_68_128) (_ bv0 1))))
(let ((?c0_128_68_128 (and ?lz_128_68_128 ?msbz_128_68_128)))
(let ((?nc0_128_68_128 (not ?c0_128_68_128)))
(let ((?c6_128_68_128 (not ?lz_128_68_128)))
(let ((?icost_128_68_128 (concat (ite ?nc0_128_68_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_68_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_72_128 (= ((_ extract 5 0) ?ltfp_128_72_128) (_ bv0 6))))
(let ((?msbz_128_72_128 (= ((_ extract 6 6) ?ltfp_128_72_128) (_ bv0 1))))
(let ((?c0_128_72_128 (and ?lz_128_72_128 ?msbz_128_72_128)))
(let ((?nc0_128_72_128 (not ?c0_128_72_128)))
(let ((?c6_128_72_128 (not ?lz_128_72_128)))
(let ((?icost_128_72_128 (concat (ite ?nc0_128_72_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_72_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_76_128 (= ((_ extract 5 0) ?ltfp_128_76_128) (_ bv0 6))))
(let ((?msbz_128_76_128 (= ((_ extract 6 6) ?ltfp_128_76_128) (_ bv0 1))))
(let ((?c0_128_76_128 (and ?lz_128_76_128 ?msbz_128_76_128)))
(let ((?nc0_128_76_128 (not ?c0_128_76_128)))
(let ((?c6_128_76_128 (not ?lz_128_76_128)))
(let ((?icost_128_76_128 (concat (ite ?nc0_128_76_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_76_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_80_128 (= ((_ extract 5 0) ?ltfp_128_80_128) (_ bv0 6))))
(let ((?msbz_128_80_128 (= ((_ extract 6 6) ?ltfp_128_80_128) (_ bv0 1))))
(let ((?c0_128_80_128 (and ?lz_128_80_128 ?msbz_128_80_128)))
(let ((?nc0_128_80_128 (not ?c0_128_80_128)))
(let ((?c6_128_80_128 (not ?lz_128_80_128)))
(let ((?icost_128_80_128 (concat (ite ?nc0_128_80_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_80_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_84_128 (= ((_ extract 5 0) ?ltfp_128_84_128) (_ bv0 6))))
(let ((?msbz_128_84_128 (= ((_ extract 6 6) ?ltfp_128_84_128) (_ bv0 1))))
(let ((?c0_128_84_128 (and ?lz_128_84_128 ?msbz_128_84_128)))
(let ((?nc0_128_84_128 (not ?c0_128_84_128)))
(let ((?c6_128_84_128 (not ?lz_128_84_128)))
(let ((?icost_128_84_128 (concat (ite ?nc0_128_84_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_84_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_88_128 (= ((_ extract 5 0) ?ltfp_128_88_128) (_ bv0 6))))
(let ((?msbz_128_88_128 (= ((_ extract 6 6) ?ltfp_128_88_128) (_ bv0 1))))
(let ((?c0_128_88_128 (and ?lz_128_88_128 ?msbz_128_88_128)))
(let ((?nc0_128_88_128 (not ?c0_128_88_128)))
(let ((?c6_128_88_128 (not ?lz_128_88_128)))
(let ((?icost_128_88_128 (concat (ite ?nc0_128_88_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_88_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_92_128 (= ((_ extract 5 0) ?ltfp_128_92_128) (_ bv0 6))))
(let ((?msbz_128_92_128 (= ((_ extract 6 6) ?ltfp_128_92_128) (_ bv0 1))))
(let ((?c0_128_92_128 (and ?lz_128_92_128 ?msbz_128_92_128)))
(let ((?nc0_128_92_128 (not ?c0_128_92_128)))
(let ((?c6_128_92_128 (not ?lz_128_92_128)))
(let ((?icost_128_92_128 (concat (ite ?nc0_128_92_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_92_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_96_128 (= ((_ extract 5 0) ?ltfp_128_96_128) (_ bv0 6))))
(let ((?msbz_128_96_128 (= ((_ extract 6 6) ?ltfp_128_96_128) (_ bv0 1))))
(let ((?c0_128_96_128 (and ?lz_128_96_128 ?msbz_128_96_128)))
(let ((?nc0_128_96_128 (not ?c0_128_96_128)))
(let ((?c6_128_96_128 (not ?lz_128_96_128)))
(let ((?icost_128_96_128 (concat (ite ?nc0_128_96_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_96_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_100_128 (= ((_ extract 5 0) ?ltfp_128_100_128) (_ bv0 6))))
(let ((?msbz_128_100_128 (= ((_ extract 6 6) ?ltfp_128_100_128) (_ bv0 1))))
(let ((?c0_128_100_128 (and ?lz_128_100_128 ?msbz_128_100_128)))
(let ((?nc0_128_100_128 (not ?c0_128_100_128)))
(let ((?c6_128_100_128 (not ?lz_128_100_128)))
(let ((?icost_128_100_128 (concat (ite ?nc0_128_100_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_100_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_104_128 (= ((_ extract 5 0) ?ltfp_128_104_128) (_ bv0 6))))
(let ((?msbz_128_104_128 (= ((_ extract 6 6) ?ltfp_128_104_128) (_ bv0 1))))
(let ((?c0_128_104_128 (and ?lz_128_104_128 ?msbz_128_104_128)))
(let ((?nc0_128_104_128 (not ?c0_128_104_128)))
(let ((?c6_128_104_128 (not ?lz_128_104_128)))
(let ((?icost_128_104_128 (concat (ite ?nc0_128_104_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_104_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_108_128 (= ((_ extract 5 0) ?ltfp_128_108_128) (_ bv0 6))))
(let ((?msbz_128_108_128 (= ((_ extract 6 6) ?ltfp_128_108_128) (_ bv0 1))))
(let ((?c0_128_108_128 (and ?lz_128_108_128 ?msbz_128_108_128)))
(let ((?nc0_128_108_128 (not ?c0_128_108_128)))
(let ((?c6_128_108_128 (not ?lz_128_108_128)))
(let ((?icost_128_108_128 (concat (ite ?nc0_128_108_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_108_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_112_128 (= ((_ extract 5 0) ?ltfp_128_112_128) (_ bv0 6))))
(let ((?msbz_128_112_128 (= ((_ extract 6 6) ?ltfp_128_112_128) (_ bv0 1))))
(let ((?c0_128_112_128 (and ?lz_128_112_128 ?msbz_128_112_128)))
(let ((?nc0_128_112_128 (not ?c0_128_112_128)))
(let ((?c6_128_112_128 (not ?lz_128_112_128)))
(let ((?icost_128_112_128 (concat (ite ?nc0_128_112_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_112_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_116_128 (= ((_ extract 5 0) ?ltfp_128_116_128) (_ bv0 6))))
(let ((?msbz_128_116_128 (= ((_ extract 6 6) ?ltfp_128_116_128) (_ bv0 1))))
(let ((?c0_128_116_128 (and ?lz_128_116_128 ?msbz_128_116_128)))
(let ((?nc0_128_116_128 (not ?c0_128_116_128)))
(let ((?c6_128_116_128 (not ?lz_128_116_128)))
(let ((?icost_128_116_128 (concat (ite ?nc0_128_116_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_116_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_120_128 (= ((_ extract 5 0) ?ltfp_128_120_128) (_ bv0 6))))
(let ((?msbz_128_120_128 (= ((_ extract 6 6) ?ltfp_128_120_128) (_ bv0 1))))
(let ((?c0_128_120_128 (and ?lz_128_120_128 ?msbz_128_120_128)))
(let ((?nc0_128_120_128 (not ?c0_128_120_128)))
(let ((?c6_128_120_128 (not ?lz_128_120_128)))
(let ((?icost_128_120_128 (concat (ite ?nc0_128_120_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_120_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_128_124_128 (= ((_ extract 5 0) ?ltfp_128_124_128) (_ bv0 6))))
(let ((?msbz_128_124_128 (= ((_ extract 6 6) ?ltfp_128_124_128) (_ bv0 1))))
(let ((?c0_128_124_128 (and ?lz_128_124_128 ?msbz_128_124_128)))
(let ((?nc0_128_124_128 (not ?c0_128_124_128)))
(let ((?c6_128_124_128 (not ?lz_128_124_128)))
(let ((?icost_128_124_128 (concat (ite ?nc0_128_124_128 (_ bv1 1) (_ bv0 1)) (ite ?c6_128_124_128 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_0_64 (= ((_ extract 5 0) ?ltfp_64_0_64) (_ bv0 6))))
(let ((?msbz_64_0_64 (= ((_ extract 6 6) ?ltfp_64_0_64) (_ bv0 1))))
(let ((?c0_64_0_64 (and ?lz_64_0_64 ?msbz_64_0_64)))
(let ((?nc0_64_0_64 (not ?c0_64_0_64)))
(let ((?c6_64_0_64 (not ?lz_64_0_64)))
(let ((?icost_64_0_64 (concat (ite ?nc0_64_0_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_0_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_4_64 (= ((_ extract 5 0) ?ltfp_64_4_64) (_ bv0 6))))
(let ((?msbz_64_4_64 (= ((_ extract 6 6) ?ltfp_64_4_64) (_ bv0 1))))
(let ((?c0_64_4_64 (and ?lz_64_4_64 ?msbz_64_4_64)))
(let ((?nc0_64_4_64 (not ?c0_64_4_64)))
(let ((?c6_64_4_64 (not ?lz_64_4_64)))
(let ((?icost_64_4_64 (concat (ite ?nc0_64_4_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_4_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_8_64 (= ((_ extract 5 0) ?ltfp_64_8_64) (_ bv0 6))))
(let ((?msbz_64_8_64 (= ((_ extract 6 6) ?ltfp_64_8_64) (_ bv0 1))))
(let ((?c0_64_8_64 (and ?lz_64_8_64 ?msbz_64_8_64)))
(let ((?nc0_64_8_64 (not ?c0_64_8_64)))
(let ((?c6_64_8_64 (not ?lz_64_8_64)))
(let ((?icost_64_8_64 (concat (ite ?nc0_64_8_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_8_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_12_64 (= ((_ extract 5 0) ?ltfp_64_12_64) (_ bv0 6))))
(let ((?msbz_64_12_64 (= ((_ extract 6 6) ?ltfp_64_12_64) (_ bv0 1))))
(let ((?c0_64_12_64 (and ?lz_64_12_64 ?msbz_64_12_64)))
(let ((?nc0_64_12_64 (not ?c0_64_12_64)))
(let ((?c6_64_12_64 (not ?lz_64_12_64)))
(let ((?icost_64_12_64 (concat (ite ?nc0_64_12_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_12_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_16_64 (= ((_ extract 5 0) ?ltfp_64_16_64) (_ bv0 6))))
(let ((?msbz_64_16_64 (= ((_ extract 6 6) ?ltfp_64_16_64) (_ bv0 1))))
(let ((?c0_64_16_64 (and ?lz_64_16_64 ?msbz_64_16_64)))
(let ((?nc0_64_16_64 (not ?c0_64_16_64)))
(let ((?c6_64_16_64 (not ?lz_64_16_64)))
(let ((?icost_64_16_64 (concat (ite ?nc0_64_16_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_16_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_20_64 (= ((_ extract 5 0) ?ltfp_64_20_64) (_ bv0 6))))
(let ((?msbz_64_20_64 (= ((_ extract 6 6) ?ltfp_64_20_64) (_ bv0 1))))
(let ((?c0_64_20_64 (and ?lz_64_20_64 ?msbz_64_20_64)))
(let ((?nc0_64_20_64 (not ?c0_64_20_64)))
(let ((?c6_64_20_64 (not ?lz_64_20_64)))
(let ((?icost_64_20_64 (concat (ite ?nc0_64_20_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_20_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_24_64 (= ((_ extract 5 0) ?ltfp_64_24_64) (_ bv0 6))))
(let ((?msbz_64_24_64 (= ((_ extract 6 6) ?ltfp_64_24_64) (_ bv0 1))))
(let ((?c0_64_24_64 (and ?lz_64_24_64 ?msbz_64_24_64)))
(let ((?nc0_64_24_64 (not ?c0_64_24_64)))
(let ((?c6_64_24_64 (not ?lz_64_24_64)))
(let ((?icost_64_24_64 (concat (ite ?nc0_64_24_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_24_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_28_64 (= ((_ extract 5 0) ?ltfp_64_28_64) (_ bv0 6))))
(let ((?msbz_64_28_64 (= ((_ extract 6 6) ?ltfp_64_28_64) (_ bv0 1))))
(let ((?c0_64_28_64 (and ?lz_64_28_64 ?msbz_64_28_64)))
(let ((?nc0_64_28_64 (not ?c0_64_28_64)))
(let ((?c6_64_28_64 (not ?lz_64_28_64)))
(let ((?icost_64_28_64 (concat (ite ?nc0_64_28_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_28_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_32_64 (= ((_ extract 5 0) ?ltfp_64_32_64) (_ bv0 6))))
(let ((?msbz_64_32_64 (= ((_ extract 6 6) ?ltfp_64_32_64) (_ bv0 1))))
(let ((?c0_64_32_64 (and ?lz_64_32_64 ?msbz_64_32_64)))
(let ((?nc0_64_32_64 (not ?c0_64_32_64)))
(let ((?c6_64_32_64 (not ?lz_64_32_64)))
(let ((?icost_64_32_64 (concat (ite ?nc0_64_32_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_32_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_36_64 (= ((_ extract 5 0) ?ltfp_64_36_64) (_ bv0 6))))
(let ((?msbz_64_36_64 (= ((_ extract 6 6) ?ltfp_64_36_64) (_ bv0 1))))
(let ((?c0_64_36_64 (and ?lz_64_36_64 ?msbz_64_36_64)))
(let ((?nc0_64_36_64 (not ?c0_64_36_64)))
(let ((?c6_64_36_64 (not ?lz_64_36_64)))
(let ((?icost_64_36_64 (concat (ite ?nc0_64_36_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_36_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_40_64 (= ((_ extract 5 0) ?ltfp_64_40_64) (_ bv0 6))))
(let ((?msbz_64_40_64 (= ((_ extract 6 6) ?ltfp_64_40_64) (_ bv0 1))))
(let ((?c0_64_40_64 (and ?lz_64_40_64 ?msbz_64_40_64)))
(let ((?nc0_64_40_64 (not ?c0_64_40_64)))
(let ((?c6_64_40_64 (not ?lz_64_40_64)))
(let ((?icost_64_40_64 (concat (ite ?nc0_64_40_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_40_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_44_64 (= ((_ extract 5 0) ?ltfp_64_44_64) (_ bv0 6))))
(let ((?msbz_64_44_64 (= ((_ extract 6 6) ?ltfp_64_44_64) (_ bv0 1))))
(let ((?c0_64_44_64 (and ?lz_64_44_64 ?msbz_64_44_64)))
(let ((?nc0_64_44_64 (not ?c0_64_44_64)))
(let ((?c6_64_44_64 (not ?lz_64_44_64)))
(let ((?icost_64_44_64 (concat (ite ?nc0_64_44_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_44_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_48_64 (= ((_ extract 5 0) ?ltfp_64_48_64) (_ bv0 6))))
(let ((?msbz_64_48_64 (= ((_ extract 6 6) ?ltfp_64_48_64) (_ bv0 1))))
(let ((?c0_64_48_64 (and ?lz_64_48_64 ?msbz_64_48_64)))
(let ((?nc0_64_48_64 (not ?c0_64_48_64)))
(let ((?c6_64_48_64 (not ?lz_64_48_64)))
(let ((?icost_64_48_64 (concat (ite ?nc0_64_48_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_48_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_52_64 (= ((_ extract 5 0) ?ltfp_64_52_64) (_ bv0 6))))
(let ((?msbz_64_52_64 (= ((_ extract 6 6) ?ltfp_64_52_64) (_ bv0 1))))
(let ((?c0_64_52_64 (and ?lz_64_52_64 ?msbz_64_52_64)))
(let ((?nc0_64_52_64 (not ?c0_64_52_64)))
(let ((?c6_64_52_64 (not ?lz_64_52_64)))
(let ((?icost_64_52_64 (concat (ite ?nc0_64_52_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_52_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_56_64 (= ((_ extract 5 0) ?ltfp_64_56_64) (_ bv0 6))))
(let ((?msbz_64_56_64 (= ((_ extract 6 6) ?ltfp_64_56_64) (_ bv0 1))))
(let ((?c0_64_56_64 (and ?lz_64_56_64 ?msbz_64_56_64)))
(let ((?nc0_64_56_64 (not ?c0_64_56_64)))
(let ((?c6_64_56_64 (not ?lz_64_56_64)))
(let ((?icost_64_56_64 (concat (ite ?nc0_64_56_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_56_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_60_64 (= ((_ extract 5 0) ?ltfp_64_60_64) (_ bv0 6))))
(let ((?msbz_64_60_64 (= ((_ extract 6 6) ?ltfp_64_60_64) (_ bv0 1))))
(let ((?c0_64_60_64 (and ?lz_64_60_64 ?msbz_64_60_64)))
(let ((?nc0_64_60_64 (not ?c0_64_60_64)))
(let ((?c6_64_60_64 (not ?lz_64_60_64)))
(let ((?icost_64_60_64 (concat (ite ?nc0_64_60_64 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_60_64 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_0_320 (= ((_ extract 5 0) ?ltfp_64_0_320) (_ bv0 6))))
(let ((?msbz_64_0_320 (= ((_ extract 6 6) ?ltfp_64_0_320) (_ bv0 1))))
(let ((?c0_64_0_320 (and ?lz_64_0_320 ?msbz_64_0_320)))
(let ((?nc0_64_0_320 (not ?c0_64_0_320)))
(let ((?c6_64_0_320 (not ?lz_64_0_320)))
(let ((?icost_64_0_320 (concat (ite ?nc0_64_0_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_0_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_4_320 (= ((_ extract 5 0) ?ltfp_64_4_320) (_ bv0 6))))
(let ((?msbz_64_4_320 (= ((_ extract 6 6) ?ltfp_64_4_320) (_ bv0 1))))
(let ((?c0_64_4_320 (and ?lz_64_4_320 ?msbz_64_4_320)))
(let ((?nc0_64_4_320 (not ?c0_64_4_320)))
(let ((?c6_64_4_320 (not ?lz_64_4_320)))
(let ((?icost_64_4_320 (concat (ite ?nc0_64_4_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_4_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_8_320 (= ((_ extract 5 0) ?ltfp_64_8_320) (_ bv0 6))))
(let ((?msbz_64_8_320 (= ((_ extract 6 6) ?ltfp_64_8_320) (_ bv0 1))))
(let ((?c0_64_8_320 (and ?lz_64_8_320 ?msbz_64_8_320)))
(let ((?nc0_64_8_320 (not ?c0_64_8_320)))
(let ((?c6_64_8_320 (not ?lz_64_8_320)))
(let ((?icost_64_8_320 (concat (ite ?nc0_64_8_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_8_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_12_320 (= ((_ extract 5 0) ?ltfp_64_12_320) (_ bv0 6))))
(let ((?msbz_64_12_320 (= ((_ extract 6 6) ?ltfp_64_12_320) (_ bv0 1))))
(let ((?c0_64_12_320 (and ?lz_64_12_320 ?msbz_64_12_320)))
(let ((?nc0_64_12_320 (not ?c0_64_12_320)))
(let ((?c6_64_12_320 (not ?lz_64_12_320)))
(let ((?icost_64_12_320 (concat (ite ?nc0_64_12_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_12_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_16_320 (= ((_ extract 5 0) ?ltfp_64_16_320) (_ bv0 6))))
(let ((?msbz_64_16_320 (= ((_ extract 6 6) ?ltfp_64_16_320) (_ bv0 1))))
(let ((?c0_64_16_320 (and ?lz_64_16_320 ?msbz_64_16_320)))
(let ((?nc0_64_16_320 (not ?c0_64_16_320)))
(let ((?c6_64_16_320 (not ?lz_64_16_320)))
(let ((?icost_64_16_320 (concat (ite ?nc0_64_16_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_16_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_20_320 (= ((_ extract 5 0) ?ltfp_64_20_320) (_ bv0 6))))
(let ((?msbz_64_20_320 (= ((_ extract 6 6) ?ltfp_64_20_320) (_ bv0 1))))
(let ((?c0_64_20_320 (and ?lz_64_20_320 ?msbz_64_20_320)))
(let ((?nc0_64_20_320 (not ?c0_64_20_320)))
(let ((?c6_64_20_320 (not ?lz_64_20_320)))
(let ((?icost_64_20_320 (concat (ite ?nc0_64_20_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_20_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_24_320 (= ((_ extract 5 0) ?ltfp_64_24_320) (_ bv0 6))))
(let ((?msbz_64_24_320 (= ((_ extract 6 6) ?ltfp_64_24_320) (_ bv0 1))))
(let ((?c0_64_24_320 (and ?lz_64_24_320 ?msbz_64_24_320)))
(let ((?nc0_64_24_320 (not ?c0_64_24_320)))
(let ((?c6_64_24_320 (not ?lz_64_24_320)))
(let ((?icost_64_24_320 (concat (ite ?nc0_64_24_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_24_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_28_320 (= ((_ extract 5 0) ?ltfp_64_28_320) (_ bv0 6))))
(let ((?msbz_64_28_320 (= ((_ extract 6 6) ?ltfp_64_28_320) (_ bv0 1))))
(let ((?c0_64_28_320 (and ?lz_64_28_320 ?msbz_64_28_320)))
(let ((?nc0_64_28_320 (not ?c0_64_28_320)))
(let ((?c6_64_28_320 (not ?lz_64_28_320)))
(let ((?icost_64_28_320 (concat (ite ?nc0_64_28_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_28_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_32_320 (= ((_ extract 5 0) ?ltfp_64_32_320) (_ bv0 6))))
(let ((?msbz_64_32_320 (= ((_ extract 6 6) ?ltfp_64_32_320) (_ bv0 1))))
(let ((?c0_64_32_320 (and ?lz_64_32_320 ?msbz_64_32_320)))
(let ((?nc0_64_32_320 (not ?c0_64_32_320)))
(let ((?c6_64_32_320 (not ?lz_64_32_320)))
(let ((?icost_64_32_320 (concat (ite ?nc0_64_32_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_32_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_36_320 (= ((_ extract 5 0) ?ltfp_64_36_320) (_ bv0 6))))
(let ((?msbz_64_36_320 (= ((_ extract 6 6) ?ltfp_64_36_320) (_ bv0 1))))
(let ((?c0_64_36_320 (and ?lz_64_36_320 ?msbz_64_36_320)))
(let ((?nc0_64_36_320 (not ?c0_64_36_320)))
(let ((?c6_64_36_320 (not ?lz_64_36_320)))
(let ((?icost_64_36_320 (concat (ite ?nc0_64_36_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_36_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_40_320 (= ((_ extract 5 0) ?ltfp_64_40_320) (_ bv0 6))))
(let ((?msbz_64_40_320 (= ((_ extract 6 6) ?ltfp_64_40_320) (_ bv0 1))))
(let ((?c0_64_40_320 (and ?lz_64_40_320 ?msbz_64_40_320)))
(let ((?nc0_64_40_320 (not ?c0_64_40_320)))
(let ((?c6_64_40_320 (not ?lz_64_40_320)))
(let ((?icost_64_40_320 (concat (ite ?nc0_64_40_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_40_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_44_320 (= ((_ extract 5 0) ?ltfp_64_44_320) (_ bv0 6))))
(let ((?msbz_64_44_320 (= ((_ extract 6 6) ?ltfp_64_44_320) (_ bv0 1))))
(let ((?c0_64_44_320 (and ?lz_64_44_320 ?msbz_64_44_320)))
(let ((?nc0_64_44_320 (not ?c0_64_44_320)))
(let ((?c6_64_44_320 (not ?lz_64_44_320)))
(let ((?icost_64_44_320 (concat (ite ?nc0_64_44_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_44_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_48_320 (= ((_ extract 5 0) ?ltfp_64_48_320) (_ bv0 6))))
(let ((?msbz_64_48_320 (= ((_ extract 6 6) ?ltfp_64_48_320) (_ bv0 1))))
(let ((?c0_64_48_320 (and ?lz_64_48_320 ?msbz_64_48_320)))
(let ((?nc0_64_48_320 (not ?c0_64_48_320)))
(let ((?c6_64_48_320 (not ?lz_64_48_320)))
(let ((?icost_64_48_320 (concat (ite ?nc0_64_48_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_48_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_52_320 (= ((_ extract 5 0) ?ltfp_64_52_320) (_ bv0 6))))
(let ((?msbz_64_52_320 (= ((_ extract 6 6) ?ltfp_64_52_320) (_ bv0 1))))
(let ((?c0_64_52_320 (and ?lz_64_52_320 ?msbz_64_52_320)))
(let ((?nc0_64_52_320 (not ?c0_64_52_320)))
(let ((?c6_64_52_320 (not ?lz_64_52_320)))
(let ((?icost_64_52_320 (concat (ite ?nc0_64_52_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_52_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_56_320 (= ((_ extract 5 0) ?ltfp_64_56_320) (_ bv0 6))))
(let ((?msbz_64_56_320 (= ((_ extract 6 6) ?ltfp_64_56_320) (_ bv0 1))))
(let ((?c0_64_56_320 (and ?lz_64_56_320 ?msbz_64_56_320)))
(let ((?nc0_64_56_320 (not ?c0_64_56_320)))
(let ((?c6_64_56_320 (not ?lz_64_56_320)))
(let ((?icost_64_56_320 (concat (ite ?nc0_64_56_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_56_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_64_60_320 (= ((_ extract 5 0) ?ltfp_64_60_320) (_ bv0 6))))
(let ((?msbz_64_60_320 (= ((_ extract 6 6) ?ltfp_64_60_320) (_ bv0 1))))
(let ((?c0_64_60_320 (and ?lz_64_60_320 ?msbz_64_60_320)))
(let ((?nc0_64_60_320 (not ?c0_64_60_320)))
(let ((?c6_64_60_320 (not ?lz_64_60_320)))
(let ((?icost_64_60_320 (concat (ite ?nc0_64_60_320 (_ bv1 1) (_ bv0 1)) (ite ?c6_64_60_320 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_0_32 (= ((_ extract 5 0) ?ltfp_32_0_32) (_ bv0 6))))
(let ((?msbz_32_0_32 (= ((_ extract 6 6) ?ltfp_32_0_32) (_ bv0 1))))
(let ((?c0_32_0_32 (and ?lz_32_0_32 ?msbz_32_0_32)))
(let ((?nc0_32_0_32 (not ?c0_32_0_32)))
(let ((?c6_32_0_32 (not ?lz_32_0_32)))
(let ((?icost_32_0_32 (concat (ite ?nc0_32_0_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_0_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_4_32 (= ((_ extract 5 0) ?ltfp_32_4_32) (_ bv0 6))))
(let ((?msbz_32_4_32 (= ((_ extract 6 6) ?ltfp_32_4_32) (_ bv0 1))))
(let ((?c0_32_4_32 (and ?lz_32_4_32 ?msbz_32_4_32)))
(let ((?nc0_32_4_32 (not ?c0_32_4_32)))
(let ((?c6_32_4_32 (not ?lz_32_4_32)))
(let ((?icost_32_4_32 (concat (ite ?nc0_32_4_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_4_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_8_32 (= ((_ extract 5 0) ?ltfp_32_8_32) (_ bv0 6))))
(let ((?msbz_32_8_32 (= ((_ extract 6 6) ?ltfp_32_8_32) (_ bv0 1))))
(let ((?c0_32_8_32 (and ?lz_32_8_32 ?msbz_32_8_32)))
(let ((?nc0_32_8_32 (not ?c0_32_8_32)))
(let ((?c6_32_8_32 (not ?lz_32_8_32)))
(let ((?icost_32_8_32 (concat (ite ?nc0_32_8_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_8_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_12_32 (= ((_ extract 5 0) ?ltfp_32_12_32) (_ bv0 6))))
(let ((?msbz_32_12_32 (= ((_ extract 6 6) ?ltfp_32_12_32) (_ bv0 1))))
(let ((?c0_32_12_32 (and ?lz_32_12_32 ?msbz_32_12_32)))
(let ((?nc0_32_12_32 (not ?c0_32_12_32)))
(let ((?c6_32_12_32 (not ?lz_32_12_32)))
(let ((?icost_32_12_32 (concat (ite ?nc0_32_12_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_12_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_16_32 (= ((_ extract 5 0) ?ltfp_32_16_32) (_ bv0 6))))
(let ((?msbz_32_16_32 (= ((_ extract 6 6) ?ltfp_32_16_32) (_ bv0 1))))
(let ((?c0_32_16_32 (and ?lz_32_16_32 ?msbz_32_16_32)))
(let ((?nc0_32_16_32 (not ?c0_32_16_32)))
(let ((?c6_32_16_32 (not ?lz_32_16_32)))
(let ((?icost_32_16_32 (concat (ite ?nc0_32_16_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_16_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_20_32 (= ((_ extract 5 0) ?ltfp_32_20_32) (_ bv0 6))))
(let ((?msbz_32_20_32 (= ((_ extract 6 6) ?ltfp_32_20_32) (_ bv0 1))))
(let ((?c0_32_20_32 (and ?lz_32_20_32 ?msbz_32_20_32)))
(let ((?nc0_32_20_32 (not ?c0_32_20_32)))
(let ((?c6_32_20_32 (not ?lz_32_20_32)))
(let ((?icost_32_20_32 (concat (ite ?nc0_32_20_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_20_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_24_32 (= ((_ extract 5 0) ?ltfp_32_24_32) (_ bv0 6))))
(let ((?msbz_32_24_32 (= ((_ extract 6 6) ?ltfp_32_24_32) (_ bv0 1))))
(let ((?c0_32_24_32 (and ?lz_32_24_32 ?msbz_32_24_32)))
(let ((?nc0_32_24_32 (not ?c0_32_24_32)))
(let ((?c6_32_24_32 (not ?lz_32_24_32)))
(let ((?icost_32_24_32 (concat (ite ?nc0_32_24_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_24_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_28_32 (= ((_ extract 5 0) ?ltfp_32_28_32) (_ bv0 6))))
(let ((?msbz_32_28_32 (= ((_ extract 6 6) ?ltfp_32_28_32) (_ bv0 1))))
(let ((?c0_32_28_32 (and ?lz_32_28_32 ?msbz_32_28_32)))
(let ((?nc0_32_28_32 (not ?c0_32_28_32)))
(let ((?c6_32_28_32 (not ?lz_32_28_32)))
(let ((?icost_32_28_32 (concat (ite ?nc0_32_28_32 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_28_32 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_0_288 (= ((_ extract 5 0) ?ltfp_32_0_288) (_ bv0 6))))
(let ((?msbz_32_0_288 (= ((_ extract 6 6) ?ltfp_32_0_288) (_ bv0 1))))
(let ((?c0_32_0_288 (and ?lz_32_0_288 ?msbz_32_0_288)))
(let ((?nc0_32_0_288 (not ?c0_32_0_288)))
(let ((?c6_32_0_288 (not ?lz_32_0_288)))
(let ((?icost_32_0_288 (concat (ite ?nc0_32_0_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_0_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_4_288 (= ((_ extract 5 0) ?ltfp_32_4_288) (_ bv0 6))))
(let ((?msbz_32_4_288 (= ((_ extract 6 6) ?ltfp_32_4_288) (_ bv0 1))))
(let ((?c0_32_4_288 (and ?lz_32_4_288 ?msbz_32_4_288)))
(let ((?nc0_32_4_288 (not ?c0_32_4_288)))
(let ((?c6_32_4_288 (not ?lz_32_4_288)))
(let ((?icost_32_4_288 (concat (ite ?nc0_32_4_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_4_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_8_288 (= ((_ extract 5 0) ?ltfp_32_8_288) (_ bv0 6))))
(let ((?msbz_32_8_288 (= ((_ extract 6 6) ?ltfp_32_8_288) (_ bv0 1))))
(let ((?c0_32_8_288 (and ?lz_32_8_288 ?msbz_32_8_288)))
(let ((?nc0_32_8_288 (not ?c0_32_8_288)))
(let ((?c6_32_8_288 (not ?lz_32_8_288)))
(let ((?icost_32_8_288 (concat (ite ?nc0_32_8_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_8_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_12_288 (= ((_ extract 5 0) ?ltfp_32_12_288) (_ bv0 6))))
(let ((?msbz_32_12_288 (= ((_ extract 6 6) ?ltfp_32_12_288) (_ bv0 1))))
(let ((?c0_32_12_288 (and ?lz_32_12_288 ?msbz_32_12_288)))
(let ((?nc0_32_12_288 (not ?c0_32_12_288)))
(let ((?c6_32_12_288 (not ?lz_32_12_288)))
(let ((?icost_32_12_288 (concat (ite ?nc0_32_12_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_12_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_16_288 (= ((_ extract 5 0) ?ltfp_32_16_288) (_ bv0 6))))
(let ((?msbz_32_16_288 (= ((_ extract 6 6) ?ltfp_32_16_288) (_ bv0 1))))
(let ((?c0_32_16_288 (and ?lz_32_16_288 ?msbz_32_16_288)))
(let ((?nc0_32_16_288 (not ?c0_32_16_288)))
(let ((?c6_32_16_288 (not ?lz_32_16_288)))
(let ((?icost_32_16_288 (concat (ite ?nc0_32_16_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_16_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_20_288 (= ((_ extract 5 0) ?ltfp_32_20_288) (_ bv0 6))))
(let ((?msbz_32_20_288 (= ((_ extract 6 6) ?ltfp_32_20_288) (_ bv0 1))))
(let ((?c0_32_20_288 (and ?lz_32_20_288 ?msbz_32_20_288)))
(let ((?nc0_32_20_288 (not ?c0_32_20_288)))
(let ((?c6_32_20_288 (not ?lz_32_20_288)))
(let ((?icost_32_20_288 (concat (ite ?nc0_32_20_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_20_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_24_288 (= ((_ extract 5 0) ?ltfp_32_24_288) (_ bv0 6))))
(let ((?msbz_32_24_288 (= ((_ extract 6 6) ?ltfp_32_24_288) (_ bv0 1))))
(let ((?c0_32_24_288 (and ?lz_32_24_288 ?msbz_32_24_288)))
(let ((?nc0_32_24_288 (not ?c0_32_24_288)))
(let ((?c6_32_24_288 (not ?lz_32_24_288)))
(let ((?icost_32_24_288 (concat (ite ?nc0_32_24_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_24_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_28_288 (= ((_ extract 5 0) ?ltfp_32_28_288) (_ bv0 6))))
(let ((?msbz_32_28_288 (= ((_ extract 6 6) ?ltfp_32_28_288) (_ bv0 1))))
(let ((?c0_32_28_288 (and ?lz_32_28_288 ?msbz_32_28_288)))
(let ((?nc0_32_28_288 (not ?c0_32_28_288)))
(let ((?c6_32_28_288 (not ?lz_32_28_288)))
(let ((?icost_32_28_288 (concat (ite ?nc0_32_28_288 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_28_288 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_0_160 (= ((_ extract 5 0) ?ltfp_32_0_160) (_ bv0 6))))
(let ((?msbz_32_0_160 (= ((_ extract 6 6) ?ltfp_32_0_160) (_ bv0 1))))
(let ((?c0_32_0_160 (and ?lz_32_0_160 ?msbz_32_0_160)))
(let ((?nc0_32_0_160 (not ?c0_32_0_160)))
(let ((?c6_32_0_160 (not ?lz_32_0_160)))
(let ((?icost_32_0_160 (concat (ite ?nc0_32_0_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_0_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_4_160 (= ((_ extract 5 0) ?ltfp_32_4_160) (_ bv0 6))))
(let ((?msbz_32_4_160 (= ((_ extract 6 6) ?ltfp_32_4_160) (_ bv0 1))))
(let ((?c0_32_4_160 (and ?lz_32_4_160 ?msbz_32_4_160)))
(let ((?nc0_32_4_160 (not ?c0_32_4_160)))
(let ((?c6_32_4_160 (not ?lz_32_4_160)))
(let ((?icost_32_4_160 (concat (ite ?nc0_32_4_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_4_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_8_160 (= ((_ extract 5 0) ?ltfp_32_8_160) (_ bv0 6))))
(let ((?msbz_32_8_160 (= ((_ extract 6 6) ?ltfp_32_8_160) (_ bv0 1))))
(let ((?c0_32_8_160 (and ?lz_32_8_160 ?msbz_32_8_160)))
(let ((?nc0_32_8_160 (not ?c0_32_8_160)))
(let ((?c6_32_8_160 (not ?lz_32_8_160)))
(let ((?icost_32_8_160 (concat (ite ?nc0_32_8_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_8_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_12_160 (= ((_ extract 5 0) ?ltfp_32_12_160) (_ bv0 6))))
(let ((?msbz_32_12_160 (= ((_ extract 6 6) ?ltfp_32_12_160) (_ bv0 1))))
(let ((?c0_32_12_160 (and ?lz_32_12_160 ?msbz_32_12_160)))
(let ((?nc0_32_12_160 (not ?c0_32_12_160)))
(let ((?c6_32_12_160 (not ?lz_32_12_160)))
(let ((?icost_32_12_160 (concat (ite ?nc0_32_12_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_12_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_16_160 (= ((_ extract 5 0) ?ltfp_32_16_160) (_ bv0 6))))
(let ((?msbz_32_16_160 (= ((_ extract 6 6) ?ltfp_32_16_160) (_ bv0 1))))
(let ((?c0_32_16_160 (and ?lz_32_16_160 ?msbz_32_16_160)))
(let ((?nc0_32_16_160 (not ?c0_32_16_160)))
(let ((?c6_32_16_160 (not ?lz_32_16_160)))
(let ((?icost_32_16_160 (concat (ite ?nc0_32_16_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_16_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_20_160 (= ((_ extract 5 0) ?ltfp_32_20_160) (_ bv0 6))))
(let ((?msbz_32_20_160 (= ((_ extract 6 6) ?ltfp_32_20_160) (_ bv0 1))))
(let ((?c0_32_20_160 (and ?lz_32_20_160 ?msbz_32_20_160)))
(let ((?nc0_32_20_160 (not ?c0_32_20_160)))
(let ((?c6_32_20_160 (not ?lz_32_20_160)))
(let ((?icost_32_20_160 (concat (ite ?nc0_32_20_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_20_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_24_160 (= ((_ extract 5 0) ?ltfp_32_24_160) (_ bv0 6))))
(let ((?msbz_32_24_160 (= ((_ extract 6 6) ?ltfp_32_24_160) (_ bv0 1))))
(let ((?c0_32_24_160 (and ?lz_32_24_160 ?msbz_32_24_160)))
(let ((?nc0_32_24_160 (not ?c0_32_24_160)))
(let ((?c6_32_24_160 (not ?lz_32_24_160)))
(let ((?icost_32_24_160 (concat (ite ?nc0_32_24_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_24_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_28_160 (= ((_ extract 5 0) ?ltfp_32_28_160) (_ bv0 6))))
(let ((?msbz_32_28_160 (= ((_ extract 6 6) ?ltfp_32_28_160) (_ bv0 1))))
(let ((?c0_32_28_160 (and ?lz_32_28_160 ?msbz_32_28_160)))
(let ((?nc0_32_28_160 (not ?c0_32_28_160)))
(let ((?c6_32_28_160 (not ?lz_32_28_160)))
(let ((?icost_32_28_160 (concat (ite ?nc0_32_28_160 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_28_160 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_0_416 (= ((_ extract 5 0) ?ltfp_32_0_416) (_ bv0 6))))
(let ((?msbz_32_0_416 (= ((_ extract 6 6) ?ltfp_32_0_416) (_ bv0 1))))
(let ((?c0_32_0_416 (and ?lz_32_0_416 ?msbz_32_0_416)))
(let ((?nc0_32_0_416 (not ?c0_32_0_416)))
(let ((?c6_32_0_416 (not ?lz_32_0_416)))
(let ((?icost_32_0_416 (concat (ite ?nc0_32_0_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_0_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_4_416 (= ((_ extract 5 0) ?ltfp_32_4_416) (_ bv0 6))))
(let ((?msbz_32_4_416 (= ((_ extract 6 6) ?ltfp_32_4_416) (_ bv0 1))))
(let ((?c0_32_4_416 (and ?lz_32_4_416 ?msbz_32_4_416)))
(let ((?nc0_32_4_416 (not ?c0_32_4_416)))
(let ((?c6_32_4_416 (not ?lz_32_4_416)))
(let ((?icost_32_4_416 (concat (ite ?nc0_32_4_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_4_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_8_416 (= ((_ extract 5 0) ?ltfp_32_8_416) (_ bv0 6))))
(let ((?msbz_32_8_416 (= ((_ extract 6 6) ?ltfp_32_8_416) (_ bv0 1))))
(let ((?c0_32_8_416 (and ?lz_32_8_416 ?msbz_32_8_416)))
(let ((?nc0_32_8_416 (not ?c0_32_8_416)))
(let ((?c6_32_8_416 (not ?lz_32_8_416)))
(let ((?icost_32_8_416 (concat (ite ?nc0_32_8_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_8_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_12_416 (= ((_ extract 5 0) ?ltfp_32_12_416) (_ bv0 6))))
(let ((?msbz_32_12_416 (= ((_ extract 6 6) ?ltfp_32_12_416) (_ bv0 1))))
(let ((?c0_32_12_416 (and ?lz_32_12_416 ?msbz_32_12_416)))
(let ((?nc0_32_12_416 (not ?c0_32_12_416)))
(let ((?c6_32_12_416 (not ?lz_32_12_416)))
(let ((?icost_32_12_416 (concat (ite ?nc0_32_12_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_12_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_16_416 (= ((_ extract 5 0) ?ltfp_32_16_416) (_ bv0 6))))
(let ((?msbz_32_16_416 (= ((_ extract 6 6) ?ltfp_32_16_416) (_ bv0 1))))
(let ((?c0_32_16_416 (and ?lz_32_16_416 ?msbz_32_16_416)))
(let ((?nc0_32_16_416 (not ?c0_32_16_416)))
(let ((?c6_32_16_416 (not ?lz_32_16_416)))
(let ((?icost_32_16_416 (concat (ite ?nc0_32_16_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_16_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_20_416 (= ((_ extract 5 0) ?ltfp_32_20_416) (_ bv0 6))))
(let ((?msbz_32_20_416 (= ((_ extract 6 6) ?ltfp_32_20_416) (_ bv0 1))))
(let ((?c0_32_20_416 (and ?lz_32_20_416 ?msbz_32_20_416)))
(let ((?nc0_32_20_416 (not ?c0_32_20_416)))
(let ((?c6_32_20_416 (not ?lz_32_20_416)))
(let ((?icost_32_20_416 (concat (ite ?nc0_32_20_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_20_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_24_416 (= ((_ extract 5 0) ?ltfp_32_24_416) (_ bv0 6))))
(let ((?msbz_32_24_416 (= ((_ extract 6 6) ?ltfp_32_24_416) (_ bv0 1))))
(let ((?c0_32_24_416 (and ?lz_32_24_416 ?msbz_32_24_416)))
(let ((?nc0_32_24_416 (not ?c0_32_24_416)))
(let ((?c6_32_24_416 (not ?lz_32_24_416)))
(let ((?icost_32_24_416 (concat (ite ?nc0_32_24_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_24_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_32_28_416 (= ((_ extract 5 0) ?ltfp_32_28_416) (_ bv0 6))))
(let ((?msbz_32_28_416 (= ((_ extract 6 6) ?ltfp_32_28_416) (_ bv0 1))))
(let ((?c0_32_28_416 (and ?lz_32_28_416 ?msbz_32_28_416)))
(let ((?nc0_32_28_416 (not ?c0_32_28_416)))
(let ((?c6_32_28_416 (not ?lz_32_28_416)))
(let ((?icost_32_28_416 (concat (ite ?nc0_32_28_416 (_ bv1 1) (_ bv0 1)) (ite ?c6_32_28_416 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_16 (= ((_ extract 5 0) ?ltfp_16_0_16) (_ bv0 6))))
(let ((?msbz_16_0_16 (= ((_ extract 6 6) ?ltfp_16_0_16) (_ bv0 1))))
(let ((?c0_16_0_16 (and ?lz_16_0_16 ?msbz_16_0_16)))
(let ((?nc0_16_0_16 (not ?c0_16_0_16)))
(let ((?c6_16_0_16 (not ?lz_16_0_16)))
(let ((?icost_16_0_16 (concat (ite ?nc0_16_0_16 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_16 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_16 (= ((_ extract 5 0) ?ltfp_16_4_16) (_ bv0 6))))
(let ((?msbz_16_4_16 (= ((_ extract 6 6) ?ltfp_16_4_16) (_ bv0 1))))
(let ((?c0_16_4_16 (and ?lz_16_4_16 ?msbz_16_4_16)))
(let ((?nc0_16_4_16 (not ?c0_16_4_16)))
(let ((?c6_16_4_16 (not ?lz_16_4_16)))
(let ((?icost_16_4_16 (concat (ite ?nc0_16_4_16 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_16 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_16 (= ((_ extract 5 0) ?ltfp_16_8_16) (_ bv0 6))))
(let ((?msbz_16_8_16 (= ((_ extract 6 6) ?ltfp_16_8_16) (_ bv0 1))))
(let ((?c0_16_8_16 (and ?lz_16_8_16 ?msbz_16_8_16)))
(let ((?nc0_16_8_16 (not ?c0_16_8_16)))
(let ((?c6_16_8_16 (not ?lz_16_8_16)))
(let ((?icost_16_8_16 (concat (ite ?nc0_16_8_16 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_16 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_16 (= ((_ extract 5 0) ?ltfp_16_12_16) (_ bv0 6))))
(let ((?msbz_16_12_16 (= ((_ extract 6 6) ?ltfp_16_12_16) (_ bv0 1))))
(let ((?c0_16_12_16 (and ?lz_16_12_16 ?msbz_16_12_16)))
(let ((?nc0_16_12_16 (not ?c0_16_12_16)))
(let ((?c6_16_12_16 (not ?lz_16_12_16)))
(let ((?icost_16_12_16 (concat (ite ?nc0_16_12_16 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_16 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_272 (= ((_ extract 5 0) ?ltfp_16_0_272) (_ bv0 6))))
(let ((?msbz_16_0_272 (= ((_ extract 6 6) ?ltfp_16_0_272) (_ bv0 1))))
(let ((?c0_16_0_272 (and ?lz_16_0_272 ?msbz_16_0_272)))
(let ((?nc0_16_0_272 (not ?c0_16_0_272)))
(let ((?c6_16_0_272 (not ?lz_16_0_272)))
(let ((?icost_16_0_272 (concat (ite ?nc0_16_0_272 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_272 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_272 (= ((_ extract 5 0) ?ltfp_16_4_272) (_ bv0 6))))
(let ((?msbz_16_4_272 (= ((_ extract 6 6) ?ltfp_16_4_272) (_ bv0 1))))
(let ((?c0_16_4_272 (and ?lz_16_4_272 ?msbz_16_4_272)))
(let ((?nc0_16_4_272 (not ?c0_16_4_272)))
(let ((?c6_16_4_272 (not ?lz_16_4_272)))
(let ((?icost_16_4_272 (concat (ite ?nc0_16_4_272 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_272 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_272 (= ((_ extract 5 0) ?ltfp_16_8_272) (_ bv0 6))))
(let ((?msbz_16_8_272 (= ((_ extract 6 6) ?ltfp_16_8_272) (_ bv0 1))))
(let ((?c0_16_8_272 (and ?lz_16_8_272 ?msbz_16_8_272)))
(let ((?nc0_16_8_272 (not ?c0_16_8_272)))
(let ((?c6_16_8_272 (not ?lz_16_8_272)))
(let ((?icost_16_8_272 (concat (ite ?nc0_16_8_272 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_272 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_272 (= ((_ extract 5 0) ?ltfp_16_12_272) (_ bv0 6))))
(let ((?msbz_16_12_272 (= ((_ extract 6 6) ?ltfp_16_12_272) (_ bv0 1))))
(let ((?c0_16_12_272 (and ?lz_16_12_272 ?msbz_16_12_272)))
(let ((?nc0_16_12_272 (not ?c0_16_12_272)))
(let ((?c6_16_12_272 (not ?lz_16_12_272)))
(let ((?icost_16_12_272 (concat (ite ?nc0_16_12_272 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_272 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_144 (= ((_ extract 5 0) ?ltfp_16_0_144) (_ bv0 6))))
(let ((?msbz_16_0_144 (= ((_ extract 6 6) ?ltfp_16_0_144) (_ bv0 1))))
(let ((?c0_16_0_144 (and ?lz_16_0_144 ?msbz_16_0_144)))
(let ((?nc0_16_0_144 (not ?c0_16_0_144)))
(let ((?c6_16_0_144 (not ?lz_16_0_144)))
(let ((?icost_16_0_144 (concat (ite ?nc0_16_0_144 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_144 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_144 (= ((_ extract 5 0) ?ltfp_16_4_144) (_ bv0 6))))
(let ((?msbz_16_4_144 (= ((_ extract 6 6) ?ltfp_16_4_144) (_ bv0 1))))
(let ((?c0_16_4_144 (and ?lz_16_4_144 ?msbz_16_4_144)))
(let ((?nc0_16_4_144 (not ?c0_16_4_144)))
(let ((?c6_16_4_144 (not ?lz_16_4_144)))
(let ((?icost_16_4_144 (concat (ite ?nc0_16_4_144 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_144 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_144 (= ((_ extract 5 0) ?ltfp_16_8_144) (_ bv0 6))))
(let ((?msbz_16_8_144 (= ((_ extract 6 6) ?ltfp_16_8_144) (_ bv0 1))))
(let ((?c0_16_8_144 (and ?lz_16_8_144 ?msbz_16_8_144)))
(let ((?nc0_16_8_144 (not ?c0_16_8_144)))
(let ((?c6_16_8_144 (not ?lz_16_8_144)))
(let ((?icost_16_8_144 (concat (ite ?nc0_16_8_144 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_144 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_144 (= ((_ extract 5 0) ?ltfp_16_12_144) (_ bv0 6))))
(let ((?msbz_16_12_144 (= ((_ extract 6 6) ?ltfp_16_12_144) (_ bv0 1))))
(let ((?c0_16_12_144 (and ?lz_16_12_144 ?msbz_16_12_144)))
(let ((?nc0_16_12_144 (not ?c0_16_12_144)))
(let ((?c6_16_12_144 (not ?lz_16_12_144)))
(let ((?icost_16_12_144 (concat (ite ?nc0_16_12_144 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_144 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_400 (= ((_ extract 5 0) ?ltfp_16_0_400) (_ bv0 6))))
(let ((?msbz_16_0_400 (= ((_ extract 6 6) ?ltfp_16_0_400) (_ bv0 1))))
(let ((?c0_16_0_400 (and ?lz_16_0_400 ?msbz_16_0_400)))
(let ((?nc0_16_0_400 (not ?c0_16_0_400)))
(let ((?c6_16_0_400 (not ?lz_16_0_400)))
(let ((?icost_16_0_400 (concat (ite ?nc0_16_0_400 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_400 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_400 (= ((_ extract 5 0) ?ltfp_16_4_400) (_ bv0 6))))
(let ((?msbz_16_4_400 (= ((_ extract 6 6) ?ltfp_16_4_400) (_ bv0 1))))
(let ((?c0_16_4_400 (and ?lz_16_4_400 ?msbz_16_4_400)))
(let ((?nc0_16_4_400 (not ?c0_16_4_400)))
(let ((?c6_16_4_400 (not ?lz_16_4_400)))
(let ((?icost_16_4_400 (concat (ite ?nc0_16_4_400 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_400 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_400 (= ((_ extract 5 0) ?ltfp_16_8_400) (_ bv0 6))))
(let ((?msbz_16_8_400 (= ((_ extract 6 6) ?ltfp_16_8_400) (_ bv0 1))))
(let ((?c0_16_8_400 (and ?lz_16_8_400 ?msbz_16_8_400)))
(let ((?nc0_16_8_400 (not ?c0_16_8_400)))
(let ((?c6_16_8_400 (not ?lz_16_8_400)))
(let ((?icost_16_8_400 (concat (ite ?nc0_16_8_400 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_400 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_400 (= ((_ extract 5 0) ?ltfp_16_12_400) (_ bv0 6))))
(let ((?msbz_16_12_400 (= ((_ extract 6 6) ?ltfp_16_12_400) (_ bv0 1))))
(let ((?c0_16_12_400 (and ?lz_16_12_400 ?msbz_16_12_400)))
(let ((?nc0_16_12_400 (not ?c0_16_12_400)))
(let ((?c6_16_12_400 (not ?lz_16_12_400)))
(let ((?icost_16_12_400 (concat (ite ?nc0_16_12_400 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_400 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_80 (= ((_ extract 5 0) ?ltfp_16_0_80) (_ bv0 6))))
(let ((?msbz_16_0_80 (= ((_ extract 6 6) ?ltfp_16_0_80) (_ bv0 1))))
(let ((?c0_16_0_80 (and ?lz_16_0_80 ?msbz_16_0_80)))
(let ((?nc0_16_0_80 (not ?c0_16_0_80)))
(let ((?c6_16_0_80 (not ?lz_16_0_80)))
(let ((?icost_16_0_80 (concat (ite ?nc0_16_0_80 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_80 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_80 (= ((_ extract 5 0) ?ltfp_16_4_80) (_ bv0 6))))
(let ((?msbz_16_4_80 (= ((_ extract 6 6) ?ltfp_16_4_80) (_ bv0 1))))
(let ((?c0_16_4_80 (and ?lz_16_4_80 ?msbz_16_4_80)))
(let ((?nc0_16_4_80 (not ?c0_16_4_80)))
(let ((?c6_16_4_80 (not ?lz_16_4_80)))
(let ((?icost_16_4_80 (concat (ite ?nc0_16_4_80 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_80 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_80 (= ((_ extract 5 0) ?ltfp_16_8_80) (_ bv0 6))))
(let ((?msbz_16_8_80 (= ((_ extract 6 6) ?ltfp_16_8_80) (_ bv0 1))))
(let ((?c0_16_8_80 (and ?lz_16_8_80 ?msbz_16_8_80)))
(let ((?nc0_16_8_80 (not ?c0_16_8_80)))
(let ((?c6_16_8_80 (not ?lz_16_8_80)))
(let ((?icost_16_8_80 (concat (ite ?nc0_16_8_80 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_80 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_80 (= ((_ extract 5 0) ?ltfp_16_12_80) (_ bv0 6))))
(let ((?msbz_16_12_80 (= ((_ extract 6 6) ?ltfp_16_12_80) (_ bv0 1))))
(let ((?c0_16_12_80 (and ?lz_16_12_80 ?msbz_16_12_80)))
(let ((?nc0_16_12_80 (not ?c0_16_12_80)))
(let ((?c6_16_12_80 (not ?lz_16_12_80)))
(let ((?icost_16_12_80 (concat (ite ?nc0_16_12_80 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_80 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_336 (= ((_ extract 5 0) ?ltfp_16_0_336) (_ bv0 6))))
(let ((?msbz_16_0_336 (= ((_ extract 6 6) ?ltfp_16_0_336) (_ bv0 1))))
(let ((?c0_16_0_336 (and ?lz_16_0_336 ?msbz_16_0_336)))
(let ((?nc0_16_0_336 (not ?c0_16_0_336)))
(let ((?c6_16_0_336 (not ?lz_16_0_336)))
(let ((?icost_16_0_336 (concat (ite ?nc0_16_0_336 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_336 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_336 (= ((_ extract 5 0) ?ltfp_16_4_336) (_ bv0 6))))
(let ((?msbz_16_4_336 (= ((_ extract 6 6) ?ltfp_16_4_336) (_ bv0 1))))
(let ((?c0_16_4_336 (and ?lz_16_4_336 ?msbz_16_4_336)))
(let ((?nc0_16_4_336 (not ?c0_16_4_336)))
(let ((?c6_16_4_336 (not ?lz_16_4_336)))
(let ((?icost_16_4_336 (concat (ite ?nc0_16_4_336 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_336 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_336 (= ((_ extract 5 0) ?ltfp_16_8_336) (_ bv0 6))))
(let ((?msbz_16_8_336 (= ((_ extract 6 6) ?ltfp_16_8_336) (_ bv0 1))))
(let ((?c0_16_8_336 (and ?lz_16_8_336 ?msbz_16_8_336)))
(let ((?nc0_16_8_336 (not ?c0_16_8_336)))
(let ((?c6_16_8_336 (not ?lz_16_8_336)))
(let ((?icost_16_8_336 (concat (ite ?nc0_16_8_336 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_336 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_336 (= ((_ extract 5 0) ?ltfp_16_12_336) (_ bv0 6))))
(let ((?msbz_16_12_336 (= ((_ extract 6 6) ?ltfp_16_12_336) (_ bv0 1))))
(let ((?c0_16_12_336 (and ?lz_16_12_336 ?msbz_16_12_336)))
(let ((?nc0_16_12_336 (not ?c0_16_12_336)))
(let ((?c6_16_12_336 (not ?lz_16_12_336)))
(let ((?icost_16_12_336 (concat (ite ?nc0_16_12_336 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_336 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_208 (= ((_ extract 5 0) ?ltfp_16_0_208) (_ bv0 6))))
(let ((?msbz_16_0_208 (= ((_ extract 6 6) ?ltfp_16_0_208) (_ bv0 1))))
(let ((?c0_16_0_208 (and ?lz_16_0_208 ?msbz_16_0_208)))
(let ((?nc0_16_0_208 (not ?c0_16_0_208)))
(let ((?c6_16_0_208 (not ?lz_16_0_208)))
(let ((?icost_16_0_208 (concat (ite ?nc0_16_0_208 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_208 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_208 (= ((_ extract 5 0) ?ltfp_16_4_208) (_ bv0 6))))
(let ((?msbz_16_4_208 (= ((_ extract 6 6) ?ltfp_16_4_208) (_ bv0 1))))
(let ((?c0_16_4_208 (and ?lz_16_4_208 ?msbz_16_4_208)))
(let ((?nc0_16_4_208 (not ?c0_16_4_208)))
(let ((?c6_16_4_208 (not ?lz_16_4_208)))
(let ((?icost_16_4_208 (concat (ite ?nc0_16_4_208 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_208 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_208 (= ((_ extract 5 0) ?ltfp_16_8_208) (_ bv0 6))))
(let ((?msbz_16_8_208 (= ((_ extract 6 6) ?ltfp_16_8_208) (_ bv0 1))))
(let ((?c0_16_8_208 (and ?lz_16_8_208 ?msbz_16_8_208)))
(let ((?nc0_16_8_208 (not ?c0_16_8_208)))
(let ((?c6_16_8_208 (not ?lz_16_8_208)))
(let ((?icost_16_8_208 (concat (ite ?nc0_16_8_208 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_208 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_208 (= ((_ extract 5 0) ?ltfp_16_12_208) (_ bv0 6))))
(let ((?msbz_16_12_208 (= ((_ extract 6 6) ?ltfp_16_12_208) (_ bv0 1))))
(let ((?c0_16_12_208 (and ?lz_16_12_208 ?msbz_16_12_208)))
(let ((?nc0_16_12_208 (not ?c0_16_12_208)))
(let ((?c6_16_12_208 (not ?lz_16_12_208)))
(let ((?icost_16_12_208 (concat (ite ?nc0_16_12_208 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_208 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_0_464 (= ((_ extract 5 0) ?ltfp_16_0_464) (_ bv0 6))))
(let ((?msbz_16_0_464 (= ((_ extract 6 6) ?ltfp_16_0_464) (_ bv0 1))))
(let ((?c0_16_0_464 (and ?lz_16_0_464 ?msbz_16_0_464)))
(let ((?nc0_16_0_464 (not ?c0_16_0_464)))
(let ((?c6_16_0_464 (not ?lz_16_0_464)))
(let ((?icost_16_0_464 (concat (ite ?nc0_16_0_464 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_0_464 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_4_464 (= ((_ extract 5 0) ?ltfp_16_4_464) (_ bv0 6))))
(let ((?msbz_16_4_464 (= ((_ extract 6 6) ?ltfp_16_4_464) (_ bv0 1))))
(let ((?c0_16_4_464 (and ?lz_16_4_464 ?msbz_16_4_464)))
(let ((?nc0_16_4_464 (not ?c0_16_4_464)))
(let ((?c6_16_4_464 (not ?lz_16_4_464)))
(let ((?icost_16_4_464 (concat (ite ?nc0_16_4_464 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_4_464 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_8_464 (= ((_ extract 5 0) ?ltfp_16_8_464) (_ bv0 6))))
(let ((?msbz_16_8_464 (= ((_ extract 6 6) ?ltfp_16_8_464) (_ bv0 1))))
(let ((?c0_16_8_464 (and ?lz_16_8_464 ?msbz_16_8_464)))
(let ((?nc0_16_8_464 (not ?c0_16_8_464)))
(let ((?c6_16_8_464 (not ?lz_16_8_464)))
(let ((?icost_16_8_464 (concat (ite ?nc0_16_8_464 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_8_464 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_16_12_464 (= ((_ extract 5 0) ?ltfp_16_12_464) (_ bv0 6))))
(let ((?msbz_16_12_464 (= ((_ extract 6 6) ?ltfp_16_12_464) (_ bv0 1))))
(let ((?c0_16_12_464 (and ?lz_16_12_464 ?msbz_16_12_464)))
(let ((?nc0_16_12_464 (not ?c0_16_12_464)))
(let ((?c6_16_12_464 (not ?lz_16_12_464)))
(let ((?icost_16_12_464 (concat (ite ?nc0_16_12_464 (_ bv1 1) (_ bv0 1)) (ite ?c6_16_12_464 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_8 (= ((_ extract 5 0) ?ltfp_8_0_8) (_ bv0 6))))
(let ((?msbz_8_0_8 (= ((_ extract 6 6) ?ltfp_8_0_8) (_ bv0 1))))
(let ((?c0_8_0_8 (and ?lz_8_0_8 ?msbz_8_0_8)))
(let ((?nc0_8_0_8 (not ?c0_8_0_8)))
(let ((?c6_8_0_8 (not ?lz_8_0_8)))
(let ((?icost_8_0_8 (concat (ite ?nc0_8_0_8 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_8 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_8 (= ((_ extract 5 0) ?ltfp_8_4_8) (_ bv0 6))))
(let ((?msbz_8_4_8 (= ((_ extract 6 6) ?ltfp_8_4_8) (_ bv0 1))))
(let ((?c0_8_4_8 (and ?lz_8_4_8 ?msbz_8_4_8)))
(let ((?nc0_8_4_8 (not ?c0_8_4_8)))
(let ((?c6_8_4_8 (not ?lz_8_4_8)))
(let ((?icost_8_4_8 (concat (ite ?nc0_8_4_8 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_8 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_264 (= ((_ extract 5 0) ?ltfp_8_0_264) (_ bv0 6))))
(let ((?msbz_8_0_264 (= ((_ extract 6 6) ?ltfp_8_0_264) (_ bv0 1))))
(let ((?c0_8_0_264 (and ?lz_8_0_264 ?msbz_8_0_264)))
(let ((?nc0_8_0_264 (not ?c0_8_0_264)))
(let ((?c6_8_0_264 (not ?lz_8_0_264)))
(let ((?icost_8_0_264 (concat (ite ?nc0_8_0_264 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_264 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_264 (= ((_ extract 5 0) ?ltfp_8_4_264) (_ bv0 6))))
(let ((?msbz_8_4_264 (= ((_ extract 6 6) ?ltfp_8_4_264) (_ bv0 1))))
(let ((?c0_8_4_264 (and ?lz_8_4_264 ?msbz_8_4_264)))
(let ((?nc0_8_4_264 (not ?c0_8_4_264)))
(let ((?c6_8_4_264 (not ?lz_8_4_264)))
(let ((?icost_8_4_264 (concat (ite ?nc0_8_4_264 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_264 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_136 (= ((_ extract 5 0) ?ltfp_8_0_136) (_ bv0 6))))
(let ((?msbz_8_0_136 (= ((_ extract 6 6) ?ltfp_8_0_136) (_ bv0 1))))
(let ((?c0_8_0_136 (and ?lz_8_0_136 ?msbz_8_0_136)))
(let ((?nc0_8_0_136 (not ?c0_8_0_136)))
(let ((?c6_8_0_136 (not ?lz_8_0_136)))
(let ((?icost_8_0_136 (concat (ite ?nc0_8_0_136 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_136 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_136 (= ((_ extract 5 0) ?ltfp_8_4_136) (_ bv0 6))))
(let ((?msbz_8_4_136 (= ((_ extract 6 6) ?ltfp_8_4_136) (_ bv0 1))))
(let ((?c0_8_4_136 (and ?lz_8_4_136 ?msbz_8_4_136)))
(let ((?nc0_8_4_136 (not ?c0_8_4_136)))
(let ((?c6_8_4_136 (not ?lz_8_4_136)))
(let ((?icost_8_4_136 (concat (ite ?nc0_8_4_136 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_136 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_392 (= ((_ extract 5 0) ?ltfp_8_0_392) (_ bv0 6))))
(let ((?msbz_8_0_392 (= ((_ extract 6 6) ?ltfp_8_0_392) (_ bv0 1))))
(let ((?c0_8_0_392 (and ?lz_8_0_392 ?msbz_8_0_392)))
(let ((?nc0_8_0_392 (not ?c0_8_0_392)))
(let ((?c6_8_0_392 (not ?lz_8_0_392)))
(let ((?icost_8_0_392 (concat (ite ?nc0_8_0_392 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_392 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_392 (= ((_ extract 5 0) ?ltfp_8_4_392) (_ bv0 6))))
(let ((?msbz_8_4_392 (= ((_ extract 6 6) ?ltfp_8_4_392) (_ bv0 1))))
(let ((?c0_8_4_392 (and ?lz_8_4_392 ?msbz_8_4_392)))
(let ((?nc0_8_4_392 (not ?c0_8_4_392)))
(let ((?c6_8_4_392 (not ?lz_8_4_392)))
(let ((?icost_8_4_392 (concat (ite ?nc0_8_4_392 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_392 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_72 (= ((_ extract 5 0) ?ltfp_8_0_72) (_ bv0 6))))
(let ((?msbz_8_0_72 (= ((_ extract 6 6) ?ltfp_8_0_72) (_ bv0 1))))
(let ((?c0_8_0_72 (and ?lz_8_0_72 ?msbz_8_0_72)))
(let ((?nc0_8_0_72 (not ?c0_8_0_72)))
(let ((?c6_8_0_72 (not ?lz_8_0_72)))
(let ((?icost_8_0_72 (concat (ite ?nc0_8_0_72 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_72 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_72 (= ((_ extract 5 0) ?ltfp_8_4_72) (_ bv0 6))))
(let ((?msbz_8_4_72 (= ((_ extract 6 6) ?ltfp_8_4_72) (_ bv0 1))))
(let ((?c0_8_4_72 (and ?lz_8_4_72 ?msbz_8_4_72)))
(let ((?nc0_8_4_72 (not ?c0_8_4_72)))
(let ((?c6_8_4_72 (not ?lz_8_4_72)))
(let ((?icost_8_4_72 (concat (ite ?nc0_8_4_72 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_72 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_328 (= ((_ extract 5 0) ?ltfp_8_0_328) (_ bv0 6))))
(let ((?msbz_8_0_328 (= ((_ extract 6 6) ?ltfp_8_0_328) (_ bv0 1))))
(let ((?c0_8_0_328 (and ?lz_8_0_328 ?msbz_8_0_328)))
(let ((?nc0_8_0_328 (not ?c0_8_0_328)))
(let ((?c6_8_0_328 (not ?lz_8_0_328)))
(let ((?icost_8_0_328 (concat (ite ?nc0_8_0_328 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_328 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_328 (= ((_ extract 5 0) ?ltfp_8_4_328) (_ bv0 6))))
(let ((?msbz_8_4_328 (= ((_ extract 6 6) ?ltfp_8_4_328) (_ bv0 1))))
(let ((?c0_8_4_328 (and ?lz_8_4_328 ?msbz_8_4_328)))
(let ((?nc0_8_4_328 (not ?c0_8_4_328)))
(let ((?c6_8_4_328 (not ?lz_8_4_328)))
(let ((?icost_8_4_328 (concat (ite ?nc0_8_4_328 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_328 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_200 (= ((_ extract 5 0) ?ltfp_8_0_200) (_ bv0 6))))
(let ((?msbz_8_0_200 (= ((_ extract 6 6) ?ltfp_8_0_200) (_ bv0 1))))
(let ((?c0_8_0_200 (and ?lz_8_0_200 ?msbz_8_0_200)))
(let ((?nc0_8_0_200 (not ?c0_8_0_200)))
(let ((?c6_8_0_200 (not ?lz_8_0_200)))
(let ((?icost_8_0_200 (concat (ite ?nc0_8_0_200 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_200 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_200 (= ((_ extract 5 0) ?ltfp_8_4_200) (_ bv0 6))))
(let ((?msbz_8_4_200 (= ((_ extract 6 6) ?ltfp_8_4_200) (_ bv0 1))))
(let ((?c0_8_4_200 (and ?lz_8_4_200 ?msbz_8_4_200)))
(let ((?nc0_8_4_200 (not ?c0_8_4_200)))
(let ((?c6_8_4_200 (not ?lz_8_4_200)))
(let ((?icost_8_4_200 (concat (ite ?nc0_8_4_200 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_200 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_456 (= ((_ extract 5 0) ?ltfp_8_0_456) (_ bv0 6))))
(let ((?msbz_8_0_456 (= ((_ extract 6 6) ?ltfp_8_0_456) (_ bv0 1))))
(let ((?c0_8_0_456 (and ?lz_8_0_456 ?msbz_8_0_456)))
(let ((?nc0_8_0_456 (not ?c0_8_0_456)))
(let ((?c6_8_0_456 (not ?lz_8_0_456)))
(let ((?icost_8_0_456 (concat (ite ?nc0_8_0_456 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_456 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_456 (= ((_ extract 5 0) ?ltfp_8_4_456) (_ bv0 6))))
(let ((?msbz_8_4_456 (= ((_ extract 6 6) ?ltfp_8_4_456) (_ bv0 1))))
(let ((?c0_8_4_456 (and ?lz_8_4_456 ?msbz_8_4_456)))
(let ((?nc0_8_4_456 (not ?c0_8_4_456)))
(let ((?c6_8_4_456 (not ?lz_8_4_456)))
(let ((?icost_8_4_456 (concat (ite ?nc0_8_4_456 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_456 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_40 (= ((_ extract 5 0) ?ltfp_8_0_40) (_ bv0 6))))
(let ((?msbz_8_0_40 (= ((_ extract 6 6) ?ltfp_8_0_40) (_ bv0 1))))
(let ((?c0_8_0_40 (and ?lz_8_0_40 ?msbz_8_0_40)))
(let ((?nc0_8_0_40 (not ?c0_8_0_40)))
(let ((?c6_8_0_40 (not ?lz_8_0_40)))
(let ((?icost_8_0_40 (concat (ite ?nc0_8_0_40 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_40 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_40 (= ((_ extract 5 0) ?ltfp_8_4_40) (_ bv0 6))))
(let ((?msbz_8_4_40 (= ((_ extract 6 6) ?ltfp_8_4_40) (_ bv0 1))))
(let ((?c0_8_4_40 (and ?lz_8_4_40 ?msbz_8_4_40)))
(let ((?nc0_8_4_40 (not ?c0_8_4_40)))
(let ((?c6_8_4_40 (not ?lz_8_4_40)))
(let ((?icost_8_4_40 (concat (ite ?nc0_8_4_40 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_40 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_296 (= ((_ extract 5 0) ?ltfp_8_0_296) (_ bv0 6))))
(let ((?msbz_8_0_296 (= ((_ extract 6 6) ?ltfp_8_0_296) (_ bv0 1))))
(let ((?c0_8_0_296 (and ?lz_8_0_296 ?msbz_8_0_296)))
(let ((?nc0_8_0_296 (not ?c0_8_0_296)))
(let ((?c6_8_0_296 (not ?lz_8_0_296)))
(let ((?icost_8_0_296 (concat (ite ?nc0_8_0_296 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_296 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_296 (= ((_ extract 5 0) ?ltfp_8_4_296) (_ bv0 6))))
(let ((?msbz_8_4_296 (= ((_ extract 6 6) ?ltfp_8_4_296) (_ bv0 1))))
(let ((?c0_8_4_296 (and ?lz_8_4_296 ?msbz_8_4_296)))
(let ((?nc0_8_4_296 (not ?c0_8_4_296)))
(let ((?c6_8_4_296 (not ?lz_8_4_296)))
(let ((?icost_8_4_296 (concat (ite ?nc0_8_4_296 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_296 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_168 (= ((_ extract 5 0) ?ltfp_8_0_168) (_ bv0 6))))
(let ((?msbz_8_0_168 (= ((_ extract 6 6) ?ltfp_8_0_168) (_ bv0 1))))
(let ((?c0_8_0_168 (and ?lz_8_0_168 ?msbz_8_0_168)))
(let ((?nc0_8_0_168 (not ?c0_8_0_168)))
(let ((?c6_8_0_168 (not ?lz_8_0_168)))
(let ((?icost_8_0_168 (concat (ite ?nc0_8_0_168 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_168 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_168 (= ((_ extract 5 0) ?ltfp_8_4_168) (_ bv0 6))))
(let ((?msbz_8_4_168 (= ((_ extract 6 6) ?ltfp_8_4_168) (_ bv0 1))))
(let ((?c0_8_4_168 (and ?lz_8_4_168 ?msbz_8_4_168)))
(let ((?nc0_8_4_168 (not ?c0_8_4_168)))
(let ((?c6_8_4_168 (not ?lz_8_4_168)))
(let ((?icost_8_4_168 (concat (ite ?nc0_8_4_168 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_168 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_424 (= ((_ extract 5 0) ?ltfp_8_0_424) (_ bv0 6))))
(let ((?msbz_8_0_424 (= ((_ extract 6 6) ?ltfp_8_0_424) (_ bv0 1))))
(let ((?c0_8_0_424 (and ?lz_8_0_424 ?msbz_8_0_424)))
(let ((?nc0_8_0_424 (not ?c0_8_0_424)))
(let ((?c6_8_0_424 (not ?lz_8_0_424)))
(let ((?icost_8_0_424 (concat (ite ?nc0_8_0_424 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_424 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_424 (= ((_ extract 5 0) ?ltfp_8_4_424) (_ bv0 6))))
(let ((?msbz_8_4_424 (= ((_ extract 6 6) ?ltfp_8_4_424) (_ bv0 1))))
(let ((?c0_8_4_424 (and ?lz_8_4_424 ?msbz_8_4_424)))
(let ((?nc0_8_4_424 (not ?c0_8_4_424)))
(let ((?c6_8_4_424 (not ?lz_8_4_424)))
(let ((?icost_8_4_424 (concat (ite ?nc0_8_4_424 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_424 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_104 (= ((_ extract 5 0) ?ltfp_8_0_104) (_ bv0 6))))
(let ((?msbz_8_0_104 (= ((_ extract 6 6) ?ltfp_8_0_104) (_ bv0 1))))
(let ((?c0_8_0_104 (and ?lz_8_0_104 ?msbz_8_0_104)))
(let ((?nc0_8_0_104 (not ?c0_8_0_104)))
(let ((?c6_8_0_104 (not ?lz_8_0_104)))
(let ((?icost_8_0_104 (concat (ite ?nc0_8_0_104 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_104 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_104 (= ((_ extract 5 0) ?ltfp_8_4_104) (_ bv0 6))))
(let ((?msbz_8_4_104 (= ((_ extract 6 6) ?ltfp_8_4_104) (_ bv0 1))))
(let ((?c0_8_4_104 (and ?lz_8_4_104 ?msbz_8_4_104)))
(let ((?nc0_8_4_104 (not ?c0_8_4_104)))
(let ((?c6_8_4_104 (not ?lz_8_4_104)))
(let ((?icost_8_4_104 (concat (ite ?nc0_8_4_104 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_104 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_360 (= ((_ extract 5 0) ?ltfp_8_0_360) (_ bv0 6))))
(let ((?msbz_8_0_360 (= ((_ extract 6 6) ?ltfp_8_0_360) (_ bv0 1))))
(let ((?c0_8_0_360 (and ?lz_8_0_360 ?msbz_8_0_360)))
(let ((?nc0_8_0_360 (not ?c0_8_0_360)))
(let ((?c6_8_0_360 (not ?lz_8_0_360)))
(let ((?icost_8_0_360 (concat (ite ?nc0_8_0_360 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_360 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_360 (= ((_ extract 5 0) ?ltfp_8_4_360) (_ bv0 6))))
(let ((?msbz_8_4_360 (= ((_ extract 6 6) ?ltfp_8_4_360) (_ bv0 1))))
(let ((?c0_8_4_360 (and ?lz_8_4_360 ?msbz_8_4_360)))
(let ((?nc0_8_4_360 (not ?c0_8_4_360)))
(let ((?c6_8_4_360 (not ?lz_8_4_360)))
(let ((?icost_8_4_360 (concat (ite ?nc0_8_4_360 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_360 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_232 (= ((_ extract 5 0) ?ltfp_8_0_232) (_ bv0 6))))
(let ((?msbz_8_0_232 (= ((_ extract 6 6) ?ltfp_8_0_232) (_ bv0 1))))
(let ((?c0_8_0_232 (and ?lz_8_0_232 ?msbz_8_0_232)))
(let ((?nc0_8_0_232 (not ?c0_8_0_232)))
(let ((?c6_8_0_232 (not ?lz_8_0_232)))
(let ((?icost_8_0_232 (concat (ite ?nc0_8_0_232 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_232 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_232 (= ((_ extract 5 0) ?ltfp_8_4_232) (_ bv0 6))))
(let ((?msbz_8_4_232 (= ((_ extract 6 6) ?ltfp_8_4_232) (_ bv0 1))))
(let ((?c0_8_4_232 (and ?lz_8_4_232 ?msbz_8_4_232)))
(let ((?nc0_8_4_232 (not ?c0_8_4_232)))
(let ((?c6_8_4_232 (not ?lz_8_4_232)))
(let ((?icost_8_4_232 (concat (ite ?nc0_8_4_232 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_232 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_0_488 (= ((_ extract 5 0) ?ltfp_8_0_488) (_ bv0 6))))
(let ((?msbz_8_0_488 (= ((_ extract 6 6) ?ltfp_8_0_488) (_ bv0 1))))
(let ((?c0_8_0_488 (and ?lz_8_0_488 ?msbz_8_0_488)))
(let ((?nc0_8_0_488 (not ?c0_8_0_488)))
(let ((?c6_8_0_488 (not ?lz_8_0_488)))
(let ((?icost_8_0_488 (concat (ite ?nc0_8_0_488 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_0_488 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_8_4_488 (= ((_ extract 5 0) ?ltfp_8_4_488) (_ bv0 6))))
(let ((?msbz_8_4_488 (= ((_ extract 6 6) ?ltfp_8_4_488) (_ bv0 1))))
(let ((?c0_8_4_488 (and ?lz_8_4_488 ?msbz_8_4_488)))
(let ((?nc0_8_4_488 (not ?c0_8_4_488)))
(let ((?c6_8_4_488 (not ?lz_8_4_488)))
(let ((?icost_8_4_488 (concat (ite ?nc0_8_4_488 (_ bv1 1) (_ bv0 1)) (ite ?c6_8_4_488 (_ bv1 1) (_ bv0 1)))))
(let ((?lz_4_0_4 (= ((_ extract 5 0) ?ltfp_4_0_4) (_ bv0 6))))
(let ((?msbz_4_0_4 (= ((_ extract 6 6) ?ltfp_4_0_4) (_ bv0 1))))
(let ((?c0_4_0_4 (and ?lz_4_0_4 ?msbz_4_0_4)))
(let ((?nc0_4_0_4 (not ?c0_4_0_4)))
(let ((?c6_4_0_4 (not ?lz_4_0_4)))
(let ((?icost_4_0_4 (concat (ite ?nc0_4_0_4 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_4 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_4 ?icost_4_0_4))
(let ((?lz_4_0_260 (= ((_ extract 5 0) ?ltfp_4_0_260) (_ bv0 6))))
(let ((?msbz_4_0_260 (= ((_ extract 6 6) ?ltfp_4_0_260) (_ bv0 1))))
(let ((?c0_4_0_260 (and ?lz_4_0_260 ?msbz_4_0_260)))
(let ((?nc0_4_0_260 (not ?c0_4_0_260)))
(let ((?c6_4_0_260 (not ?lz_4_0_260)))
(let ((?icost_4_0_260 (concat (ite ?nc0_4_0_260 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_260 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_260 ?icost_4_0_260))
(let ((?lz_4_0_132 (= ((_ extract 5 0) ?ltfp_4_0_132) (_ bv0 6))))
(let ((?msbz_4_0_132 (= ((_ extract 6 6) ?ltfp_4_0_132) (_ bv0 1))))
(let ((?c0_4_0_132 (and ?lz_4_0_132 ?msbz_4_0_132)))
(let ((?nc0_4_0_132 (not ?c0_4_0_132)))
(let ((?c6_4_0_132 (not ?lz_4_0_132)))
(let ((?icost_4_0_132 (concat (ite ?nc0_4_0_132 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_132 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_132 ?icost_4_0_132))
(let ((?lz_4_0_388 (= ((_ extract 5 0) ?ltfp_4_0_388) (_ bv0 6))))
(let ((?msbz_4_0_388 (= ((_ extract 6 6) ?ltfp_4_0_388) (_ bv0 1))))
(let ((?c0_4_0_388 (and ?lz_4_0_388 ?msbz_4_0_388)))
(let ((?nc0_4_0_388 (not ?c0_4_0_388)))
(let ((?c6_4_0_388 (not ?lz_4_0_388)))
(let ((?icost_4_0_388 (concat (ite ?nc0_4_0_388 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_388 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_388 ?icost_4_0_388))
(let ((?lz_4_0_68 (= ((_ extract 5 0) ?ltfp_4_0_68) (_ bv0 6))))
(let ((?msbz_4_0_68 (= ((_ extract 6 6) ?ltfp_4_0_68) (_ bv0 1))))
(let ((?c0_4_0_68 (and ?lz_4_0_68 ?msbz_4_0_68)))
(let ((?nc0_4_0_68 (not ?c0_4_0_68)))
(let ((?c6_4_0_68 (not ?lz_4_0_68)))
(let ((?icost_4_0_68 (concat (ite ?nc0_4_0_68 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_68 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_68 ?icost_4_0_68))
(let ((?lz_4_0_324 (= ((_ extract 5 0) ?ltfp_4_0_324) (_ bv0 6))))
(let ((?msbz_4_0_324 (= ((_ extract 6 6) ?ltfp_4_0_324) (_ bv0 1))))
(let ((?c0_4_0_324 (and ?lz_4_0_324 ?msbz_4_0_324)))
(let ((?nc0_4_0_324 (not ?c0_4_0_324)))
(let ((?c6_4_0_324 (not ?lz_4_0_324)))
(let ((?icost_4_0_324 (concat (ite ?nc0_4_0_324 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_324 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_324 ?icost_4_0_324))
(let ((?lz_4_0_196 (= ((_ extract 5 0) ?ltfp_4_0_196) (_ bv0 6))))
(let ((?msbz_4_0_196 (= ((_ extract 6 6) ?ltfp_4_0_196) (_ bv0 1))))
(let ((?c0_4_0_196 (and ?lz_4_0_196 ?msbz_4_0_196)))
(let ((?nc0_4_0_196 (not ?c0_4_0_196)))
(let ((?c6_4_0_196 (not ?lz_4_0_196)))
(let ((?icost_4_0_196 (concat (ite ?nc0_4_0_196 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_196 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_196 ?icost_4_0_196))
(let ((?lz_4_0_452 (= ((_ extract 5 0) ?ltfp_4_0_452) (_ bv0 6))))
(let ((?msbz_4_0_452 (= ((_ extract 6 6) ?ltfp_4_0_452) (_ bv0 1))))
(let ((?c0_4_0_452 (and ?lz_4_0_452 ?msbz_4_0_452)))
(let ((?nc0_4_0_452 (not ?c0_4_0_452)))
(let ((?c6_4_0_452 (not ?lz_4_0_452)))
(let ((?icost_4_0_452 (concat (ite ?nc0_4_0_452 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_452 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_452 ?icost_4_0_452))
(let ((?lz_4_0_36 (= ((_ extract 5 0) ?ltfp_4_0_36) (_ bv0 6))))
(let ((?msbz_4_0_36 (= ((_ extract 6 6) ?ltfp_4_0_36) (_ bv0 1))))
(let ((?c0_4_0_36 (and ?lz_4_0_36 ?msbz_4_0_36)))
(let ((?nc0_4_0_36 (not ?c0_4_0_36)))
(let ((?c6_4_0_36 (not ?lz_4_0_36)))
(let ((?icost_4_0_36 (concat (ite ?nc0_4_0_36 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_36 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_36 ?icost_4_0_36))
(let ((?lz_4_0_292 (= ((_ extract 5 0) ?ltfp_4_0_292) (_ bv0 6))))
(let ((?msbz_4_0_292 (= ((_ extract 6 6) ?ltfp_4_0_292) (_ bv0 1))))
(let ((?c0_4_0_292 (and ?lz_4_0_292 ?msbz_4_0_292)))
(let ((?nc0_4_0_292 (not ?c0_4_0_292)))
(let ((?c6_4_0_292 (not ?lz_4_0_292)))
(let ((?icost_4_0_292 (concat (ite ?nc0_4_0_292 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_292 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_292 ?icost_4_0_292))
(let ((?lz_4_0_164 (= ((_ extract 5 0) ?ltfp_4_0_164) (_ bv0 6))))
(let ((?msbz_4_0_164 (= ((_ extract 6 6) ?ltfp_4_0_164) (_ bv0 1))))
(let ((?c0_4_0_164 (and ?lz_4_0_164 ?msbz_4_0_164)))
(let ((?nc0_4_0_164 (not ?c0_4_0_164)))
(let ((?c6_4_0_164 (not ?lz_4_0_164)))
(let ((?icost_4_0_164 (concat (ite ?nc0_4_0_164 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_164 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_164 ?icost_4_0_164))
(let ((?lz_4_0_420 (= ((_ extract 5 0) ?ltfp_4_0_420) (_ bv0 6))))
(let ((?msbz_4_0_420 (= ((_ extract 6 6) ?ltfp_4_0_420) (_ bv0 1))))
(let ((?c0_4_0_420 (and ?lz_4_0_420 ?msbz_4_0_420)))
(let ((?nc0_4_0_420 (not ?c0_4_0_420)))
(let ((?c6_4_0_420 (not ?lz_4_0_420)))
(let ((?icost_4_0_420 (concat (ite ?nc0_4_0_420 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_420 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_420 ?icost_4_0_420))
(let ((?lz_4_0_100 (= ((_ extract 5 0) ?ltfp_4_0_100) (_ bv0 6))))
(let ((?msbz_4_0_100 (= ((_ extract 6 6) ?ltfp_4_0_100) (_ bv0 1))))
(let ((?c0_4_0_100 (and ?lz_4_0_100 ?msbz_4_0_100)))
(let ((?nc0_4_0_100 (not ?c0_4_0_100)))
(let ((?c6_4_0_100 (not ?lz_4_0_100)))
(let ((?icost_4_0_100 (concat (ite ?nc0_4_0_100 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_100 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_100 ?icost_4_0_100))
(let ((?lz_4_0_356 (= ((_ extract 5 0) ?ltfp_4_0_356) (_ bv0 6))))
(let ((?msbz_4_0_356 (= ((_ extract 6 6) ?ltfp_4_0_356) (_ bv0 1))))
(let ((?c0_4_0_356 (and ?lz_4_0_356 ?msbz_4_0_356)))
(let ((?nc0_4_0_356 (not ?c0_4_0_356)))
(let ((?c6_4_0_356 (not ?lz_4_0_356)))
(let ((?icost_4_0_356 (concat (ite ?nc0_4_0_356 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_356 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_356 ?icost_4_0_356))
(let ((?lz_4_0_228 (= ((_ extract 5 0) ?ltfp_4_0_228) (_ bv0 6))))
(let ((?msbz_4_0_228 (= ((_ extract 6 6) ?ltfp_4_0_228) (_ bv0 1))))
(let ((?c0_4_0_228 (and ?lz_4_0_228 ?msbz_4_0_228)))
(let ((?nc0_4_0_228 (not ?c0_4_0_228)))
(let ((?c6_4_0_228 (not ?lz_4_0_228)))
(let ((?icost_4_0_228 (concat (ite ?nc0_4_0_228 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_228 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_228 ?icost_4_0_228))
(let ((?lz_4_0_484 (= ((_ extract 5 0) ?ltfp_4_0_484) (_ bv0 6))))
(let ((?msbz_4_0_484 (= ((_ extract 6 6) ?ltfp_4_0_484) (_ bv0 1))))
(let ((?c0_4_0_484 (and ?lz_4_0_484 ?msbz_4_0_484)))
(let ((?nc0_4_0_484 (not ?c0_4_0_484)))
(let ((?c6_4_0_484 (not ?lz_4_0_484)))
(let ((?icost_4_0_484 (concat (ite ?nc0_4_0_484 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_484 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_484 ?icost_4_0_484))
(let ((?lz_4_0_20 (= ((_ extract 5 0) ?ltfp_4_0_20) (_ bv0 6))))
(let ((?msbz_4_0_20 (= ((_ extract 6 6) ?ltfp_4_0_20) (_ bv0 1))))
(let ((?c0_4_0_20 (and ?lz_4_0_20 ?msbz_4_0_20)))
(let ((?nc0_4_0_20 (not ?c0_4_0_20)))
(let ((?c6_4_0_20 (not ?lz_4_0_20)))
(let ((?icost_4_0_20 (concat (ite ?nc0_4_0_20 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_20 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_20 ?icost_4_0_20))
(let ((?lz_4_0_276 (= ((_ extract 5 0) ?ltfp_4_0_276) (_ bv0 6))))
(let ((?msbz_4_0_276 (= ((_ extract 6 6) ?ltfp_4_0_276) (_ bv0 1))))
(let ((?c0_4_0_276 (and ?lz_4_0_276 ?msbz_4_0_276)))
(let ((?nc0_4_0_276 (not ?c0_4_0_276)))
(let ((?c6_4_0_276 (not ?lz_4_0_276)))
(let ((?icost_4_0_276 (concat (ite ?nc0_4_0_276 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_276 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_276 ?icost_4_0_276))
(let ((?lz_4_0_148 (= ((_ extract 5 0) ?ltfp_4_0_148) (_ bv0 6))))
(let ((?msbz_4_0_148 (= ((_ extract 6 6) ?ltfp_4_0_148) (_ bv0 1))))
(let ((?c0_4_0_148 (and ?lz_4_0_148 ?msbz_4_0_148)))
(let ((?nc0_4_0_148 (not ?c0_4_0_148)))
(let ((?c6_4_0_148 (not ?lz_4_0_148)))
(let ((?icost_4_0_148 (concat (ite ?nc0_4_0_148 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_148 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_148 ?icost_4_0_148))
(let ((?lz_4_0_404 (= ((_ extract 5 0) ?ltfp_4_0_404) (_ bv0 6))))
(let ((?msbz_4_0_404 (= ((_ extract 6 6) ?ltfp_4_0_404) (_ bv0 1))))
(let ((?c0_4_0_404 (and ?lz_4_0_404 ?msbz_4_0_404)))
(let ((?nc0_4_0_404 (not ?c0_4_0_404)))
(let ((?c6_4_0_404 (not ?lz_4_0_404)))
(let ((?icost_4_0_404 (concat (ite ?nc0_4_0_404 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_404 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_404 ?icost_4_0_404))
(let ((?lz_4_0_84 (= ((_ extract 5 0) ?ltfp_4_0_84) (_ bv0 6))))
(let ((?msbz_4_0_84 (= ((_ extract 6 6) ?ltfp_4_0_84) (_ bv0 1))))
(let ((?c0_4_0_84 (and ?lz_4_0_84 ?msbz_4_0_84)))
(let ((?nc0_4_0_84 (not ?c0_4_0_84)))
(let ((?c6_4_0_84 (not ?lz_4_0_84)))
(let ((?icost_4_0_84 (concat (ite ?nc0_4_0_84 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_84 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_84 ?icost_4_0_84))
(let ((?lz_4_0_340 (= ((_ extract 5 0) ?ltfp_4_0_340) (_ bv0 6))))
(let ((?msbz_4_0_340 (= ((_ extract 6 6) ?ltfp_4_0_340) (_ bv0 1))))
(let ((?c0_4_0_340 (and ?lz_4_0_340 ?msbz_4_0_340)))
(let ((?nc0_4_0_340 (not ?c0_4_0_340)))
(let ((?c6_4_0_340 (not ?lz_4_0_340)))
(let ((?icost_4_0_340 (concat (ite ?nc0_4_0_340 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_340 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_340 ?icost_4_0_340))
(let ((?lz_4_0_212 (= ((_ extract 5 0) ?ltfp_4_0_212) (_ bv0 6))))
(let ((?msbz_4_0_212 (= ((_ extract 6 6) ?ltfp_4_0_212) (_ bv0 1))))
(let ((?c0_4_0_212 (and ?lz_4_0_212 ?msbz_4_0_212)))
(let ((?nc0_4_0_212 (not ?c0_4_0_212)))
(let ((?c6_4_0_212 (not ?lz_4_0_212)))
(let ((?icost_4_0_212 (concat (ite ?nc0_4_0_212 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_212 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_212 ?icost_4_0_212))
(let ((?lz_4_0_468 (= ((_ extract 5 0) ?ltfp_4_0_468) (_ bv0 6))))
(let ((?msbz_4_0_468 (= ((_ extract 6 6) ?ltfp_4_0_468) (_ bv0 1))))
(let ((?c0_4_0_468 (and ?lz_4_0_468 ?msbz_4_0_468)))
(let ((?nc0_4_0_468 (not ?c0_4_0_468)))
(let ((?c6_4_0_468 (not ?lz_4_0_468)))
(let ((?icost_4_0_468 (concat (ite ?nc0_4_0_468 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_468 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_468 ?icost_4_0_468))
(let ((?lz_4_0_52 (= ((_ extract 5 0) ?ltfp_4_0_52) (_ bv0 6))))
(let ((?msbz_4_0_52 (= ((_ extract 6 6) ?ltfp_4_0_52) (_ bv0 1))))
(let ((?c0_4_0_52 (and ?lz_4_0_52 ?msbz_4_0_52)))
(let ((?nc0_4_0_52 (not ?c0_4_0_52)))
(let ((?c6_4_0_52 (not ?lz_4_0_52)))
(let ((?icost_4_0_52 (concat (ite ?nc0_4_0_52 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_52 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_52 ?icost_4_0_52))
(let ((?lz_4_0_308 (= ((_ extract 5 0) ?ltfp_4_0_308) (_ bv0 6))))
(let ((?msbz_4_0_308 (= ((_ extract 6 6) ?ltfp_4_0_308) (_ bv0 1))))
(let ((?c0_4_0_308 (and ?lz_4_0_308 ?msbz_4_0_308)))
(let ((?nc0_4_0_308 (not ?c0_4_0_308)))
(let ((?c6_4_0_308 (not ?lz_4_0_308)))
(let ((?icost_4_0_308 (concat (ite ?nc0_4_0_308 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_308 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_308 ?icost_4_0_308))
(let ((?lz_4_0_180 (= ((_ extract 5 0) ?ltfp_4_0_180) (_ bv0 6))))
(let ((?msbz_4_0_180 (= ((_ extract 6 6) ?ltfp_4_0_180) (_ bv0 1))))
(let ((?c0_4_0_180 (and ?lz_4_0_180 ?msbz_4_0_180)))
(let ((?nc0_4_0_180 (not ?c0_4_0_180)))
(let ((?c6_4_0_180 (not ?lz_4_0_180)))
(let ((?icost_4_0_180 (concat (ite ?nc0_4_0_180 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_180 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_180 ?icost_4_0_180))
(let ((?lz_4_0_436 (= ((_ extract 5 0) ?ltfp_4_0_436) (_ bv0 6))))
(let ((?msbz_4_0_436 (= ((_ extract 6 6) ?ltfp_4_0_436) (_ bv0 1))))
(let ((?c0_4_0_436 (and ?lz_4_0_436 ?msbz_4_0_436)))
(let ((?nc0_4_0_436 (not ?c0_4_0_436)))
(let ((?c6_4_0_436 (not ?lz_4_0_436)))
(let ((?icost_4_0_436 (concat (ite ?nc0_4_0_436 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_436 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_436 ?icost_4_0_436))
(let ((?lz_4_0_116 (= ((_ extract 5 0) ?ltfp_4_0_116) (_ bv0 6))))
(let ((?msbz_4_0_116 (= ((_ extract 6 6) ?ltfp_4_0_116) (_ bv0 1))))
(let ((?c0_4_0_116 (and ?lz_4_0_116 ?msbz_4_0_116)))
(let ((?nc0_4_0_116 (not ?c0_4_0_116)))
(let ((?c6_4_0_116 (not ?lz_4_0_116)))
(let ((?icost_4_0_116 (concat (ite ?nc0_4_0_116 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_116 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_116 ?icost_4_0_116))
(let ((?lz_4_0_372 (= ((_ extract 5 0) ?ltfp_4_0_372) (_ bv0 6))))
(let ((?msbz_4_0_372 (= ((_ extract 6 6) ?ltfp_4_0_372) (_ bv0 1))))
(let ((?c0_4_0_372 (and ?lz_4_0_372 ?msbz_4_0_372)))
(let ((?nc0_4_0_372 (not ?c0_4_0_372)))
(let ((?c6_4_0_372 (not ?lz_4_0_372)))
(let ((?icost_4_0_372 (concat (ite ?nc0_4_0_372 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_372 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_372 ?icost_4_0_372))
(let ((?lz_4_0_244 (= ((_ extract 5 0) ?ltfp_4_0_244) (_ bv0 6))))
(let ((?msbz_4_0_244 (= ((_ extract 6 6) ?ltfp_4_0_244) (_ bv0 1))))
(let ((?c0_4_0_244 (and ?lz_4_0_244 ?msbz_4_0_244)))
(let ((?nc0_4_0_244 (not ?c0_4_0_244)))
(let ((?c6_4_0_244 (not ?lz_4_0_244)))
(let ((?icost_4_0_244 (concat (ite ?nc0_4_0_244 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_244 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_244 ?icost_4_0_244))
(let ((?lz_4_0_500 (= ((_ extract 5 0) ?ltfp_4_0_500) (_ bv0 6))))
(let ((?msbz_4_0_500 (= ((_ extract 6 6) ?ltfp_4_0_500) (_ bv0 1))))
(let ((?c0_4_0_500 (and ?lz_4_0_500 ?msbz_4_0_500)))
(let ((?nc0_4_0_500 (not ?c0_4_0_500)))
(let ((?c6_4_0_500 (not ?lz_4_0_500)))
(let ((?icost_4_0_500 (concat (ite ?nc0_4_0_500 (_ bv1 1) (_ bv0 1)) (ite ?c6_4_0_500 (_ bv1 1) (_ bv0 1)))))
(let ((?tcost_4_0_500 ?icost_4_0_500))
(let ((?pinzero_128_0_128_1 (and ?c6_64_0_64 (or (or (and ?c6_128_0_128 ?c6_128_64_128) (and ?c6_128_0_128 ?c6_64_0_320)) (and ?c6_128_64_128 ?c6_64_0_320)))))
(let ((?pinzero_128_4_128_1 (and ?c6_64_4_64 (or (or (and ?c6_128_4_128 ?c6_128_68_128) (and ?c6_128_4_128 ?c6_64_4_320)) (and ?c6_128_68_128 ?c6_64_4_320)))))
(let ((?pinzero_128_8_128_1 (and ?c6_64_8_64 (or (or (and ?c6_128_8_128 ?c6_128_72_128) (and ?c6_128_8_128 ?c6_64_8_320)) (and ?c6_128_72_128 ?c6_64_8_320)))))
(let ((?pinzero_128_12_128_1 (and ?c6_64_12_64 (or (or (and ?c6_128_12_128 ?c6_128_76_128) (and ?c6_128_12_128 ?c6_64_12_320)) (and ?c6_128_76_128 ?c6_64_12_320)))))
(let ((?pinzero_128_16_128_1 (and ?c6_64_16_64 (or (or (and ?c6_128_16_128 ?c6_128_80_128) (and ?c6_128_16_128 ?c6_64_16_320)) (and ?c6_128_80_128 ?c6_64_16_320)))))
(let ((?pinzero_128_20_128_1 (and ?c6_64_20_64 (or (or (and ?c6_128_20_128 ?c6_128_84_128) (and ?c6_128_20_128 ?c6_64_20_320)) (and ?c6_128_84_128 ?c6_64_20_320)))))
(let ((?pinzero_128_24_128_1 (and ?c6_64_24_64 (or (or (and ?c6_128_24_128 ?c6_128_88_128) (and ?c6_128_24_128 ?c6_64_24_320)) (and ?c6_128_88_128 ?c6_64_24_320)))))
(let ((?pinzero_128_28_128_1 (and ?c6_64_28_64 (or (or (and ?c6_128_28_128 ?c6_128_92_128) (and ?c6_128_28_128 ?c6_64_28_320)) (and ?c6_128_92_128 ?c6_64_28_320)))))
(let ((?pinzero_128_32_128_1 (and ?c6_64_32_64 (or (or (and ?c6_128_32_128 ?c6_128_96_128) (and ?c6_128_32_128 ?c6_64_32_320)) (and ?c6_128_96_128 ?c6_64_32_320)))))
(let ((?pinzero_128_36_128_1 (and ?c6_64_36_64 (or (or (and ?c6_128_36_128 ?c6_128_100_128) (and ?c6_128_36_128 ?c6_64_36_320)) (and ?c6_128_100_128 ?c6_64_36_320)))))
(let ((?pinzero_128_40_128_1 (and ?c6_64_40_64 (or (or (and ?c6_128_40_128 ?c6_128_104_128) (and ?c6_128_40_128 ?c6_64_40_320)) (and ?c6_128_104_128 ?c6_64_40_320)))))
(let ((?pinzero_128_44_128_1 (and ?c6_64_44_64 (or (or (and ?c6_128_44_128 ?c6_128_108_128) (and ?c6_128_44_128 ?c6_64_44_320)) (and ?c6_128_108_128 ?c6_64_44_320)))))
(let ((?pinzero_128_48_128_1 (and ?c6_64_48_64 (or (or (and ?c6_128_48_128 ?c6_128_112_128) (and ?c6_128_48_128 ?c6_64_48_320)) (and ?c6_128_112_128 ?c6_64_48_320)))))
(let ((?pinzero_128_52_128_1 (and ?c6_64_52_64 (or (or (and ?c6_128_52_128 ?c6_128_116_128) (and ?c6_128_52_128 ?c6_64_52_320)) (and ?c6_128_116_128 ?c6_64_52_320)))))
(let ((?pinzero_128_56_128_1 (and ?c6_64_56_64 (or (or (and ?c6_128_56_128 ?c6_128_120_128) (and ?c6_128_56_128 ?c6_64_56_320)) (and ?c6_128_120_128 ?c6_64_56_320)))))
(let ((?pinzero_128_60_128_1 (and ?c6_64_60_64 (or (or (and ?c6_128_60_128 ?c6_128_124_128) (and ?c6_128_60_128 ?c6_64_60_320)) (and ?c6_128_124_128 ?c6_64_60_320)))))
(let ((?pinzero_64_0_64_1 (and ?c6_32_0_32 (or (or (and ?c6_64_0_64 ?c6_64_32_64) (and ?c6_64_0_64 ?c6_32_0_288)) (and ?c6_64_32_64 ?c6_32_0_288)))))
(let ((?pinzero_64_4_64_1 (and ?c6_32_4_32 (or (or (and ?c6_64_4_64 ?c6_64_36_64) (and ?c6_64_4_64 ?c6_32_4_288)) (and ?c6_64_36_64 ?c6_32_4_288)))))
(let ((?pinzero_64_8_64_1 (and ?c6_32_8_32 (or (or (and ?c6_64_8_64 ?c6_64_40_64) (and ?c6_64_8_64 ?c6_32_8_288)) (and ?c6_64_40_64 ?c6_32_8_288)))))
(let ((?pinzero_64_12_64_1 (and ?c6_32_12_32 (or (or (and ?c6_64_12_64 ?c6_64_44_64) (and ?c6_64_12_64 ?c6_32_12_288)) (and ?c6_64_44_64 ?c6_32_12_288)))))
(let ((?pinzero_64_16_64_1 (and ?c6_32_16_32 (or (or (and ?c6_64_16_64 ?c6_64_48_64) (and ?c6_64_16_64 ?c6_32_16_288)) (and ?c6_64_48_64 ?c6_32_16_288)))))
(let ((?pinzero_64_20_64_1 (and ?c6_32_20_32 (or (or (and ?c6_64_20_64 ?c6_64_52_64) (and ?c6_64_20_64 ?c6_32_20_288)) (and ?c6_64_52_64 ?c6_32_20_288)))))
(let ((?pinzero_64_24_64_1 (and ?c6_32_24_32 (or (or (and ?c6_64_24_64 ?c6_64_56_64) (and ?c6_64_24_64 ?c6_32_24_288)) (and ?c6_64_56_64 ?c6_32_24_288)))))
(let ((?pinzero_64_28_64_1 (and ?c6_32_28_32 (or (or (and ?c6_64_28_64 ?c6_64_60_64) (and ?c6_64_28_64 ?c6_32_28_288)) (and ?c6_64_60_64 ?c6_32_28_288)))))
(let ((?pinzero_64_0_320_1 (and ?c6_32_0_160 (or (or (and ?c6_64_0_320 ?c6_64_32_320) (and ?c6_64_0_320 ?c6_32_0_416)) (and ?c6_64_32_320 ?c6_32_0_416)))))
(let ((?pinzero_64_4_320_1 (and ?c6_32_4_160 (or (or (and ?c6_64_4_320 ?c6_64_36_320) (and ?c6_64_4_320 ?c6_32_4_416)) (and ?c6_64_36_320 ?c6_32_4_416)))))
(let ((?pinzero_64_8_320_1 (and ?c6_32_8_160 (or (or (and ?c6_64_8_320 ?c6_64_40_320) (and ?c6_64_8_320 ?c6_32_8_416)) (and ?c6_64_40_320 ?c6_32_8_416)))))
(let ((?pinzero_64_12_320_1 (and ?c6_32_12_160 (or (or (and ?c6_64_12_320 ?c6_64_44_320) (and ?c6_64_12_320 ?c6_32_12_416)) (and ?c6_64_44_320 ?c6_32_12_416)))))
(let ((?pinzero_64_16_320_1 (and ?c6_32_16_160 (or (or (and ?c6_64_16_320 ?c6_64_48_320) (and ?c6_64_16_320 ?c6_32_16_416)) (and ?c6_64_48_320 ?c6_32_16_416)))))
(let ((?pinzero_64_20_320_1 (and ?c6_32_20_160 (or (or (and ?c6_64_20_320 ?c6_64_52_320) (and ?c6_64_20_320 ?c6_32_20_416)) (and ?c6_64_52_320 ?c6_32_20_416)))))
(let ((?pinzero_64_24_320_1 (and ?c6_32_24_160 (or (or (and ?c6_64_24_320 ?c6_64_56_320) (and ?c6_64_24_320 ?c6_32_24_416)) (and ?c6_64_56_320 ?c6_32_24_416)))))
(let ((?pinzero_64_28_320_1 (and ?c6_32_28_160 (or (or (and ?c6_64_28_320 ?c6_64_60_320) (and ?c6_64_28_320 ?c6_32_28_416)) (and ?c6_64_60_320 ?c6_32_28_416)))))
(let ((?pinzero_32_0_32_1 (and ?c6_16_0_16 (or (or (and ?c6_32_0_32 ?c6_32_16_32) (and ?c6_32_0_32 ?c6_16_0_272)) (and ?c6_32_16_32 ?c6_16_0_272)))))
(let ((?pinzero_32_4_32_1 (and ?c6_16_4_16 (or (or (and ?c6_32_4_32 ?c6_32_20_32) (and ?c6_32_4_32 ?c6_16_4_272)) (and ?c6_32_20_32 ?c6_16_4_272)))))
(let ((?pinzero_32_8_32_1 (and ?c6_16_8_16 (or (or (and ?c6_32_8_32 ?c6_32_24_32) (and ?c6_32_8_32 ?c6_16_8_272)) (and ?c6_32_24_32 ?c6_16_8_272)))))
(let ((?pinzero_32_12_32_1 (and ?c6_16_12_16 (or (or (and ?c6_32_12_32 ?c6_32_28_32) (and ?c6_32_12_32 ?c6_16_12_272)) (and ?c6_32_28_32 ?c6_16_12_272)))))
(let ((?pinzero_32_0_288_1 (and ?c6_16_0_144 (or (or (and ?c6_32_0_288 ?c6_32_16_288) (and ?c6_32_0_288 ?c6_16_0_400)) (and ?c6_32_16_288 ?c6_16_0_400)))))
(let ((?pinzero_32_4_288_1 (and ?c6_16_4_144 (or (or (and ?c6_32_4_288 ?c6_32_20_288) (and ?c6_32_4_288 ?c6_16_4_400)) (and ?c6_32_20_288 ?c6_16_4_400)))))
(let ((?pinzero_32_8_288_1 (and ?c6_16_8_144 (or (or (and ?c6_32_8_288 ?c6_32_24_288) (and ?c6_32_8_288 ?c6_16_8_400)) (and ?c6_32_24_288 ?c6_16_8_400)))))
(let ((?pinzero_32_12_288_1 (and ?c6_16_12_144 (or (or (and ?c6_32_12_288 ?c6_32_28_288) (and ?c6_32_12_288 ?c6_16_12_400)) (and ?c6_32_28_288 ?c6_16_12_400)))))
(let ((?pinzero_32_0_160_1 (and ?c6_16_0_80 (or (or (and ?c6_32_0_160 ?c6_32_16_160) (and ?c6_32_0_160 ?c6_16_0_336)) (and ?c6_32_16_160 ?c6_16_0_336)))))
(let ((?pinzero_32_4_160_1 (and ?c6_16_4_80 (or (or (and ?c6_32_4_160 ?c6_32_20_160) (and ?c6_32_4_160 ?c6_16_4_336)) (and ?c6_32_20_160 ?c6_16_4_336)))))
(let ((?pinzero_32_8_160_1 (and ?c6_16_8_80 (or (or (and ?c6_32_8_160 ?c6_32_24_160) (and ?c6_32_8_160 ?c6_16_8_336)) (and ?c6_32_24_160 ?c6_16_8_336)))))
(let ((?pinzero_32_12_160_1 (and ?c6_16_12_80 (or (or (and ?c6_32_12_160 ?c6_32_28_160) (and ?c6_32_12_160 ?c6_16_12_336)) (and ?c6_32_28_160 ?c6_16_12_336)))))
(let ((?pinzero_32_0_416_1 (and ?c6_16_0_208 (or (or (and ?c6_32_0_416 ?c6_32_16_416) (and ?c6_32_0_416 ?c6_16_0_464)) (and ?c6_32_16_416 ?c6_16_0_464)))))
(let ((?pinzero_32_4_416_1 (and ?c6_16_4_208 (or (or (and ?c6_32_4_416 ?c6_32_20_416) (and ?c6_32_4_416 ?c6_16_4_464)) (and ?c6_32_20_416 ?c6_16_4_464)))))
(let ((?pinzero_32_8_416_1 (and ?c6_16_8_208 (or (or (and ?c6_32_8_416 ?c6_32_24_416) (and ?c6_32_8_416 ?c6_16_8_464)) (and ?c6_32_24_416 ?c6_16_8_464)))))
(let ((?pinzero_32_12_416_1 (and ?c6_16_12_208 (or (or (and ?c6_32_12_416 ?c6_32_28_416) (and ?c6_32_12_416 ?c6_16_12_464)) (and ?c6_32_28_416 ?c6_16_12_464)))))
(let ((?pinzero_16_0_16_1 (and ?c6_8_0_8 (or (or (and ?c6_16_0_16 ?c6_16_8_16) (and ?c6_16_0_16 ?c6_8_0_264)) (and ?c6_16_8_16 ?c6_8_0_264)))))
(let ((?pinzero_16_4_16_1 (and ?c6_8_4_8 (or (or (and ?c6_16_4_16 ?c6_16_12_16) (and ?c6_16_4_16 ?c6_8_4_264)) (and ?c6_16_12_16 ?c6_8_4_264)))))
(let ((?pinzero_16_0_272_1 (and ?c6_8_0_136 (or (or (and ?c6_16_0_272 ?c6_16_8_272) (and ?c6_16_0_272 ?c6_8_0_392)) (and ?c6_16_8_272 ?c6_8_0_392)))))
(let ((?pinzero_16_4_272_1 (and ?c6_8_4_136 (or (or (and ?c6_16_4_272 ?c6_16_12_272) (and ?c6_16_4_272 ?c6_8_4_392)) (and ?c6_16_12_272 ?c6_8_4_392)))))
(let ((?pinzero_16_0_144_1 (and ?c6_8_0_72 (or (or (and ?c6_16_0_144 ?c6_16_8_144) (and ?c6_16_0_144 ?c6_8_0_328)) (and ?c6_16_8_144 ?c6_8_0_328)))))
(let ((?pinzero_16_4_144_1 (and ?c6_8_4_72 (or (or (and ?c6_16_4_144 ?c6_16_12_144) (and ?c6_16_4_144 ?c6_8_4_328)) (and ?c6_16_12_144 ?c6_8_4_328)))))
(let ((?pinzero_16_0_400_1 (and ?c6_8_0_200 (or (or (and ?c6_16_0_400 ?c6_16_8_400) (and ?c6_16_0_400 ?c6_8_0_456)) (and ?c6_16_8_400 ?c6_8_0_456)))))
(let ((?pinzero_16_4_400_1 (and ?c6_8_4_200 (or (or (and ?c6_16_4_400 ?c6_16_12_400) (and ?c6_16_4_400 ?c6_8_4_456)) (and ?c6_16_12_400 ?c6_8_4_456)))))
(let ((?pinzero_16_0_80_1 (and ?c6_8_0_40 (or (or (and ?c6_16_0_80 ?c6_16_8_80) (and ?c6_16_0_80 ?c6_8_0_296)) (and ?c6_16_8_80 ?c6_8_0_296)))))
(let ((?pinzero_16_4_80_1 (and ?c6_8_4_40 (or (or (and ?c6_16_4_80 ?c6_16_12_80) (and ?c6_16_4_80 ?c6_8_4_296)) (and ?c6_16_12_80 ?c6_8_4_296)))))
(let ((?pinzero_16_0_336_1 (and ?c6_8_0_168 (or (or (and ?c6_16_0_336 ?c6_16_8_336) (and ?c6_16_0_336 ?c6_8_0_424)) (and ?c6_16_8_336 ?c6_8_0_424)))))
(let ((?pinzero_16_4_336_1 (and ?c6_8_4_168 (or (or (and ?c6_16_4_336 ?c6_16_12_336) (and ?c6_16_4_336 ?c6_8_4_424)) (and ?c6_16_12_336 ?c6_8_4_424)))))
(let ((?pinzero_16_0_208_1 (and ?c6_8_0_104 (or (or (and ?c6_16_0_208 ?c6_16_8_208) (and ?c6_16_0_208 ?c6_8_0_360)) (and ?c6_16_8_208 ?c6_8_0_360)))))
(let ((?pinzero_16_4_208_1 (and ?c6_8_4_104 (or (or (and ?c6_16_4_208 ?c6_16_12_208) (and ?c6_16_4_208 ?c6_8_4_360)) (and ?c6_16_12_208 ?c6_8_4_360)))))
(let ((?pinzero_16_0_464_1 (and ?c6_8_0_232 (or (or (and ?c6_16_0_464 ?c6_16_8_464) (and ?c6_16_0_464 ?c6_8_0_488)) (and ?c6_16_8_464 ?c6_8_0_488)))))
(let ((?pinzero_16_4_464_1 (and ?c6_8_4_232 (or (or (and ?c6_16_4_464 ?c6_16_12_464) (and ?c6_16_4_464 ?c6_8_4_488)) (and ?c6_16_12_464 ?c6_8_4_488)))))
(let ((?pinzero_8_0_8_1 (and ?c6_4_0_4 (or (or (and ?c6_8_0_8 ?c6_8_4_8) (and ?c6_8_0_8 ?c6_4_0_260)) (and ?c6_8_4_8 ?c6_4_0_260)))))
(let ((?pinzero_8_0_264_1 (and ?c6_4_0_132 (or (or (and ?c6_8_0_264 ?c6_8_4_264) (and ?c6_8_0_264 ?c6_4_0_388)) (and ?c6_8_4_264 ?c6_4_0_388)))))
(let ((?pinzero_8_0_136_1 (and ?c6_4_0_68 (or (or (and ?c6_8_0_136 ?c6_8_4_136) (and ?c6_8_0_136 ?c6_4_0_324)) (and ?c6_8_4_136 ?c6_4_0_324)))))
(let ((?pinzero_8_0_392_1 (and ?c6_4_0_196 (or (or (and ?c6_8_0_392 ?c6_8_4_392) (and ?c6_8_0_392 ?c6_4_0_452)) (and ?c6_8_4_392 ?c6_4_0_452)))))
(let ((?pinzero_8_0_72_1 (and ?c6_4_0_36 (or (or (and ?c6_8_0_72 ?c6_8_4_72) (and ?c6_8_0_72 ?c6_4_0_292)) (and ?c6_8_4_72 ?c6_4_0_292)))))
(let ((?pinzero_8_0_328_1 (and ?c6_4_0_164 (or (or (and ?c6_8_0_328 ?c6_8_4_328) (and ?c6_8_0_328 ?c6_4_0_420)) (and ?c6_8_4_328 ?c6_4_0_420)))))
(let ((?pinzero_8_0_200_1 (and ?c6_4_0_100 (or (or (and ?c6_8_0_200 ?c6_8_4_200) (and ?c6_8_0_200 ?c6_4_0_356)) (and ?c6_8_4_200 ?c6_4_0_356)))))
(let ((?pinzero_8_0_456_1 (and ?c6_4_0_228 (or (or (and ?c6_8_0_456 ?c6_8_4_456) (and ?c6_8_0_456 ?c6_4_0_484)) (and ?c6_8_4_456 ?c6_4_0_484)))))
(let ((?pinzero_8_0_40_1 (and ?c6_4_0_20 (or (or (and ?c6_8_0_40 ?c6_8_4_40) (and ?c6_8_0_40 ?c6_4_0_276)) (and ?c6_8_4_40 ?c6_4_0_276)))))
(let ((?pinzero_8_0_296_1 (and ?c6_4_0_148 (or (or (and ?c6_8_0_296 ?c6_8_4_296) (and ?c6_8_0_296 ?c6_4_0_404)) (and ?c6_8_4_296 ?c6_4_0_404)))))
(let ((?pinzero_8_0_168_1 (and ?c6_4_0_84 (or (or (and ?c6_8_0_168 ?c6_8_4_168) (and ?c6_8_0_168 ?c6_4_0_340)) (and ?c6_8_4_168 ?c6_4_0_340)))))
(let ((?pinzero_8_0_424_1 (and ?c6_4_0_212 (or (or (and ?c6_8_0_424 ?c6_8_4_424) (and ?c6_8_0_424 ?c6_4_0_468)) (and ?c6_8_4_424 ?c6_4_0_468)))))
(let ((?pinzero_8_0_104_1 (and ?c6_4_0_52 (or (or (and ?c6_8_0_104 ?c6_8_4_104) (and ?c6_8_0_104 ?c6_4_0_308)) (and ?c6_8_4_104 ?c6_4_0_308)))))
(let ((?pinzero_8_0_360_1 (and ?c6_4_0_180 (or (or (and ?c6_8_0_360 ?c6_8_4_360) (and ?c6_8_0_360 ?c6_4_0_436)) (and ?c6_8_4_360 ?c6_4_0_436)))))
(let ((?pinzero_8_0_232_1 (and ?c6_4_0_116 (or (or (and ?c6_8_0_232 ?c6_8_4_232) (and ?c6_8_0_232 ?c6_4_0_372)) (and ?c6_8_4_232 ?c6_4_0_372)))))
(let ((?pinzero_8_0_488_1 (and ?c6_4_0_244 (or (or (and ?c6_8_0_488 ?c6_8_4_488) (and ?c6_8_0_488 ?c6_4_0_500)) (and ?c6_8_4_488 ?c6_4_0_500)))))
(let ((?pushup_128_0_128_1 (and ?nc0_64_0_64 (= ?ltfp_64_0_64 ?ltfp_64_0_320))))
(let ((?pushup_128_4_128_1 (and ?nc0_64_4_64 (= ?ltfp_64_4_64 ?ltfp_64_4_320))))
(let ((?pushup_128_8_128_1 (and ?nc0_64_8_64 (= ?ltfp_64_8_64 ?ltfp_64_8_320))))
(let ((?pushup_128_12_128_1 (and ?nc0_64_12_64 (= ?ltfp_64_12_64 ?ltfp_64_12_320))))
(let ((?pushup_128_16_128_1 (and ?nc0_64_16_64 (= ?ltfp_64_16_64 ?ltfp_64_16_320))))
(let ((?pushup_128_20_128_1 (and ?nc0_64_20_64 (= ?ltfp_64_20_64 ?ltfp_64_20_320))))
(let ((?pushup_128_24_128_1 (and ?nc0_64_24_64 (= ?ltfp_64_24_64 ?ltfp_64_24_320))))
(let ((?pushup_128_28_128_1 (and ?nc0_64_28_64 (= ?ltfp_64_28_64 ?ltfp_64_28_320))))
(let ((?pushup_128_32_128_1 (and ?nc0_64_32_64 (= ?ltfp_64_32_64 ?ltfp_64_32_320))))
(let ((?pushup_128_36_128_1 (and ?nc0_64_36_64 (= ?ltfp_64_36_64 ?ltfp_64_36_320))))
(let ((?pushup_128_40_128_1 (and ?nc0_64_40_64 (= ?ltfp_64_40_64 ?ltfp_64_40_320))))
(let ((?pushup_128_44_128_1 (and ?nc0_64_44_64 (= ?ltfp_64_44_64 ?ltfp_64_44_320))))
(let ((?pushup_128_48_128_1 (and ?nc0_64_48_64 (= ?ltfp_64_48_64 ?ltfp_64_48_320))))
(let ((?pushup_128_52_128_1 (and ?nc0_64_52_64 (= ?ltfp_64_52_64 ?ltfp_64_52_320))))
(let ((?pushup_128_56_128_1 (and ?nc0_64_56_64 (= ?ltfp_64_56_64 ?ltfp_64_56_320))))
(let ((?pushup_128_60_128_1 (and ?nc0_64_60_64 (= ?ltfp_64_60_64 ?ltfp_64_60_320))))
(let ((?pushup_64_0_64_1 (and ?nc0_32_0_32 (= ?ltfp_32_0_32 ?ltfp_32_0_288))))
(let ((?pushup_64_4_64_1 (and ?nc0_32_4_32 (= ?ltfp_32_4_32 ?ltfp_32_4_288))))
(let ((?pushup_64_8_64_1 (and ?nc0_32_8_32 (= ?ltfp_32_8_32 ?ltfp_32_8_288))))
(let ((?pushup_64_12_64_1 (and ?nc0_32_12_32 (= ?ltfp_32_12_32 ?ltfp_32_12_288))))
(let ((?pushup_64_16_64_1 (and ?nc0_32_16_32 (= ?ltfp_32_16_32 ?ltfp_32_16_288))))
(let ((?pushup_64_20_64_1 (and ?nc0_32_20_32 (= ?ltfp_32_20_32 ?ltfp_32_20_288))))
(let ((?pushup_64_24_64_1 (and ?nc0_32_24_32 (= ?ltfp_32_24_32 ?ltfp_32_24_288))))
(let ((?pushup_64_28_64_1 (and ?nc0_32_28_32 (= ?ltfp_32_28_32 ?ltfp_32_28_288))))
(let ((?pushup_64_0_320_1 (and ?nc0_32_0_160 (= ?ltfp_32_0_160 ?ltfp_32_0_416))))
(let ((?pushup_64_4_320_1 (and ?nc0_32_4_160 (= ?ltfp_32_4_160 ?ltfp_32_4_416))))
(let ((?pushup_64_8_320_1 (and ?nc0_32_8_160 (= ?ltfp_32_8_160 ?ltfp_32_8_416))))
(let ((?pushup_64_12_320_1 (and ?nc0_32_12_160 (= ?ltfp_32_12_160 ?ltfp_32_12_416))))
(let ((?pushup_64_16_320_1 (and ?nc0_32_16_160 (= ?ltfp_32_16_160 ?ltfp_32_16_416))))
(let ((?pushup_64_20_320_1 (and ?nc0_32_20_160 (= ?ltfp_32_20_160 ?ltfp_32_20_416))))
(let ((?pushup_64_24_320_1 (and ?nc0_32_24_160 (= ?ltfp_32_24_160 ?ltfp_32_24_416))))
(let ((?pushup_64_28_320_1 (and ?nc0_32_28_160 (= ?ltfp_32_28_160 ?ltfp_32_28_416))))
(let ((?pushup_32_0_32_1 (and ?nc0_16_0_16 (= ?ltfp_16_0_16 ?ltfp_16_0_272))))
(let ((?pushup_32_4_32_1 (and ?nc0_16_4_16 (= ?ltfp_16_4_16 ?ltfp_16_4_272))))
(let ((?pushup_32_8_32_1 (and ?nc0_16_8_16 (= ?ltfp_16_8_16 ?ltfp_16_8_272))))
(let ((?pushup_32_12_32_1 (and ?nc0_16_12_16 (= ?ltfp_16_12_16 ?ltfp_16_12_272))))
(let ((?pushup_32_0_288_1 (and ?nc0_16_0_144 (= ?ltfp_16_0_144 ?ltfp_16_0_400))))
(let ((?pushup_32_4_288_1 (and ?nc0_16_4_144 (= ?ltfp_16_4_144 ?ltfp_16_4_400))))
(let ((?pushup_32_8_288_1 (and ?nc0_16_8_144 (= ?ltfp_16_8_144 ?ltfp_16_8_400))))
(let ((?pushup_32_12_288_1 (and ?nc0_16_12_144 (= ?ltfp_16_12_144 ?ltfp_16_12_400))))
(let ((?pushup_32_0_160_1 (and ?nc0_16_0_80 (= ?ltfp_16_0_80 ?ltfp_16_0_336))))
(let ((?pushup_32_4_160_1 (and ?nc0_16_4_80 (= ?ltfp_16_4_80 ?ltfp_16_4_336))))
(let ((?pushup_32_8_160_1 (and ?nc0_16_8_80 (= ?ltfp_16_8_80 ?ltfp_16_8_336))))
(let ((?pushup_32_12_160_1 (and ?nc0_16_12_80 (= ?ltfp_16_12_80 ?ltfp_16_12_336))))
(let ((?pushup_32_0_416_1 (and ?nc0_16_0_208 (= ?ltfp_16_0_208 ?ltfp_16_0_464))))
(let ((?pushup_32_4_416_1 (and ?nc0_16_4_208 (= ?ltfp_16_4_208 ?ltfp_16_4_464))))
(let ((?pushup_32_8_416_1 (and ?nc0_16_8_208 (= ?ltfp_16_8_208 ?ltfp_16_8_464))))
(let ((?pushup_32_12_416_1 (and ?nc0_16_12_208 (= ?ltfp_16_12_208 ?ltfp_16_12_464))))
(let ((?pushup_16_0_16_1 (and ?nc0_8_0_8 (= ?ltfp_8_0_8 ?ltfp_8_0_264))))
(let ((?pushup_16_4_16_1 (and ?nc0_8_4_8 (= ?ltfp_8_4_8 ?ltfp_8_4_264))))
(let ((?pushup_16_0_272_1 (and ?nc0_8_0_136 (= ?ltfp_8_0_136 ?ltfp_8_0_392))))
(let ((?pushup_16_4_272_1 (and ?nc0_8_4_136 (= ?ltfp_8_4_136 ?ltfp_8_4_392))))
(let ((?pushup_16_0_144_1 (and ?nc0_8_0_72 (= ?ltfp_8_0_72 ?ltfp_8_0_328))))
(let ((?pushup_16_4_144_1 (and ?nc0_8_4_72 (= ?ltfp_8_4_72 ?ltfp_8_4_328))))
(let ((?pushup_16_0_400_1 (and ?nc0_8_0_200 (= ?ltfp_8_0_200 ?ltfp_8_0_456))))
(let ((?pushup_16_4_400_1 (and ?nc0_8_4_200 (= ?ltfp_8_4_200 ?ltfp_8_4_456))))
(let ((?pushup_16_0_80_1 (and ?nc0_8_0_40 (= ?ltfp_8_0_40 ?ltfp_8_0_296))))
(let ((?pushup_16_4_80_1 (and ?nc0_8_4_40 (= ?ltfp_8_4_40 ?ltfp_8_4_296))))
(let ((?pushup_16_0_336_1 (and ?nc0_8_0_168 (= ?ltfp_8_0_168 ?ltfp_8_0_424))))
(let ((?pushup_16_4_336_1 (and ?nc0_8_4_168 (= ?ltfp_8_4_168 ?ltfp_8_4_424))))
(let ((?pushup_16_0_208_1 (and ?nc0_8_0_104 (= ?ltfp_8_0_104 ?ltfp_8_0_360))))
(let ((?pushup_16_4_208_1 (and ?nc0_8_4_104 (= ?ltfp_8_4_104 ?ltfp_8_4_360))))
(let ((?pushup_16_0_464_1 (and ?nc0_8_0_232 (= ?ltfp_8_0_232 ?ltfp_8_0_488))))
(let ((?pushup_16_4_464_1 (and ?nc0_8_4_232 (= ?ltfp_8_4_232 ?ltfp_8_4_488))))
(let ((?pushup_8_0_8_1 (and ?nc0_4_0_4 (= ?ltfp_4_0_4 ?ltfp_4_0_260))))
(let ((?pushup_8_0_264_1 (and ?nc0_4_0_132 (= ?ltfp_4_0_132 ?ltfp_4_0_388))))
(let ((?pushup_8_0_136_1 (and ?nc0_4_0_68 (= ?ltfp_4_0_68 ?ltfp_4_0_324))))
(let ((?pushup_8_0_392_1 (and ?nc0_4_0_196 (= ?ltfp_4_0_196 ?ltfp_4_0_452))))
(let ((?pushup_8_0_72_1 (and ?nc0_4_0_36 (= ?ltfp_4_0_36 ?ltfp_4_0_292))))
(let ((?pushup_8_0_328_1 (and ?nc0_4_0_164 (= ?ltfp_4_0_164 ?ltfp_4_0_420))))
(let ((?pushup_8_0_200_1 (and ?nc0_4_0_100 (= ?ltfp_4_0_100 ?ltfp_4_0_356))))
(let ((?pushup_8_0_456_1 (and ?nc0_4_0_228 (= ?ltfp_4_0_228 ?ltfp_4_0_484))))
(let ((?pushup_8_0_40_1 (and ?nc0_4_0_20 (= ?ltfp_4_0_20 ?ltfp_4_0_276))))
(let ((?pushup_8_0_296_1 (and ?nc0_4_0_148 (= ?ltfp_4_0_148 ?ltfp_4_0_404))))
(let ((?pushup_8_0_168_1 (and ?nc0_4_0_84 (= ?ltfp_4_0_84 ?ltfp_4_0_340))))
(let ((?pushup_8_0_424_1 (and ?nc0_4_0_212 (= ?ltfp_4_0_212 ?ltfp_4_0_468))))
(let ((?pushup_8_0_104_1 (and ?nc0_4_0_52 (= ?ltfp_4_0_52 ?ltfp_4_0_308))))
(let ((?pushup_8_0_360_1 (and ?nc0_4_0_180 (= ?ltfp_4_0_180 ?ltfp_4_0_436))))
(let ((?pushup_8_0_232_1 (and ?nc0_4_0_116 (= ?ltfp_4_0_116 ?ltfp_4_0_372))))
(let ((?pushup_8_0_488_1 (and ?nc0_4_0_244 (= ?ltfp_4_0_244 ?ltfp_4_0_500))))
(let ((?bcost_8_0_8_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_4) ((_ zero_extend 1) ?tcost_4_0_260))))
(let ((?icost_8_0_8_1 (bvadd ((_ zero_extend 1) ?icost_8_0_8) ((_ zero_extend 1) ?icost_8_4_8))))
(let ((?tcost_8_0_8_1 (bvadd ((_ zero_extend 1) ?icost_8_0_8_1) ((_ zero_extend 1) ?bcost_8_0_8_1))))
(let ((?bcost_8_0_264_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_132) ((_ zero_extend 1) ?tcost_4_0_388))))
(let ((?icost_8_0_264_1 (bvadd ((_ zero_extend 1) ?icost_8_0_264) ((_ zero_extend 1) ?icost_8_4_264))))
(let ((?tcost_8_0_264_1 (bvadd ((_ zero_extend 1) ?icost_8_0_264_1) ((_ zero_extend 1) ?bcost_8_0_264_1))))
(let ((?bcost_16_0_16_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_8_1) ((_ zero_extend 1) ?tcost_8_0_264_1))))
(let ((?icost_16_0_16_1 (bvadd ((_ zero_extend 1) ?icost_16_0_16) ((_ zero_extend 1) ?icost_16_8_16))))
(let ((?icost_16_4_16_1 (bvadd ((_ zero_extend 1) ?icost_16_4_16) ((_ zero_extend 1) ?icost_16_12_16))))
(let ((?icost_16_0_16_2 (bvadd ((_ zero_extend 1) ?icost_16_0_16_1) ((_ zero_extend 1) ?icost_16_4_16_1))))
(let ((?tcost_16_0_16_2 (bvadd ((_ zero_extend 2) ?icost_16_0_16_2) ((_ zero_extend 1) ?bcost_16_0_16_2))))
(let ((?bcost_8_0_136_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_68) ((_ zero_extend 1) ?tcost_4_0_324))))
(let ((?icost_8_0_136_1 (bvadd ((_ zero_extend 1) ?icost_8_0_136) ((_ zero_extend 1) ?icost_8_4_136))))
(let ((?tcost_8_0_136_1 (bvadd ((_ zero_extend 1) ?icost_8_0_136_1) ((_ zero_extend 1) ?bcost_8_0_136_1))))
(let ((?bcost_8_0_392_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_196) ((_ zero_extend 1) ?tcost_4_0_452))))
(let ((?icost_8_0_392_1 (bvadd ((_ zero_extend 1) ?icost_8_0_392) ((_ zero_extend 1) ?icost_8_4_392))))
(let ((?tcost_8_0_392_1 (bvadd ((_ zero_extend 1) ?icost_8_0_392_1) ((_ zero_extend 1) ?bcost_8_0_392_1))))
(let ((?bcost_16_0_272_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_136_1) ((_ zero_extend 1) ?tcost_8_0_392_1))))
(let ((?icost_16_0_272_1 (bvadd ((_ zero_extend 1) ?icost_16_0_272) ((_ zero_extend 1) ?icost_16_8_272))))
(let ((?icost_16_4_272_1 (bvadd ((_ zero_extend 1) ?icost_16_4_272) ((_ zero_extend 1) ?icost_16_12_272))))
(let ((?icost_16_0_272_2 (bvadd ((_ zero_extend 1) ?icost_16_0_272_1) ((_ zero_extend 1) ?icost_16_4_272_1))))
(let ((?tcost_16_0_272_2 (bvadd ((_ zero_extend 2) ?icost_16_0_272_2) ((_ zero_extend 1) ?bcost_16_0_272_2))))
(let ((?bcost_32_0_32_3 (bvadd ((_ zero_extend 1) ?tcost_16_0_16_2) ((_ zero_extend 1) ?tcost_16_0_272_2))))
(let ((?icost_32_0_32_1 (bvadd ((_ zero_extend 1) ?icost_32_0_32) ((_ zero_extend 1) ?icost_32_16_32))))
(let ((?icost_32_8_32_1 (bvadd ((_ zero_extend 1) ?icost_32_8_32) ((_ zero_extend 1) ?icost_32_24_32))))
(let ((?icost_32_0_32_2 (bvadd ((_ zero_extend 1) ?icost_32_0_32_1) ((_ zero_extend 1) ?icost_32_8_32_1))))
(let ((?icost_32_4_32_1 (bvadd ((_ zero_extend 1) ?icost_32_4_32) ((_ zero_extend 1) ?icost_32_20_32))))
(let ((?icost_32_12_32_1 (bvadd ((_ zero_extend 1) ?icost_32_12_32) ((_ zero_extend 1) ?icost_32_28_32))))
(let ((?icost_32_4_32_2 (bvadd ((_ zero_extend 1) ?icost_32_4_32_1) ((_ zero_extend 1) ?icost_32_12_32_1))))
(let ((?icost_32_0_32_3 (bvadd ((_ zero_extend 1) ?icost_32_0_32_2) ((_ zero_extend 1) ?icost_32_4_32_2))))
(let ((?tcost_32_0_32_3 (bvadd ((_ zero_extend 2) ?icost_32_0_32_3) ?bcost_32_0_32_3)))
(let ((?bcost_8_0_72_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_36) ((_ zero_extend 1) ?tcost_4_0_292))))
(let ((?icost_8_0_72_1 (bvadd ((_ zero_extend 1) ?icost_8_0_72) ((_ zero_extend 1) ?icost_8_4_72))))
(let ((?tcost_8_0_72_1 (bvadd ((_ zero_extend 1) ?icost_8_0_72_1) ((_ zero_extend 1) ?bcost_8_0_72_1))))
(let ((?bcost_8_0_328_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_164) ((_ zero_extend 1) ?tcost_4_0_420))))
(let ((?icost_8_0_328_1 (bvadd ((_ zero_extend 1) ?icost_8_0_328) ((_ zero_extend 1) ?icost_8_4_328))))
(let ((?tcost_8_0_328_1 (bvadd ((_ zero_extend 1) ?icost_8_0_328_1) ((_ zero_extend 1) ?bcost_8_0_328_1))))
(let ((?bcost_16_0_144_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_72_1) ((_ zero_extend 1) ?tcost_8_0_328_1))))
(let ((?icost_16_0_144_1 (bvadd ((_ zero_extend 1) ?icost_16_0_144) ((_ zero_extend 1) ?icost_16_8_144))))
(let ((?icost_16_4_144_1 (bvadd ((_ zero_extend 1) ?icost_16_4_144) ((_ zero_extend 1) ?icost_16_12_144))))
(let ((?icost_16_0_144_2 (bvadd ((_ zero_extend 1) ?icost_16_0_144_1) ((_ zero_extend 1) ?icost_16_4_144_1))))
(let ((?tcost_16_0_144_2 (bvadd ((_ zero_extend 2) ?icost_16_0_144_2) ((_ zero_extend 1) ?bcost_16_0_144_2))))
(let ((?bcost_8_0_200_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_100) ((_ zero_extend 1) ?tcost_4_0_356))))
(let ((?icost_8_0_200_1 (bvadd ((_ zero_extend 1) ?icost_8_0_200) ((_ zero_extend 1) ?icost_8_4_200))))
(let ((?tcost_8_0_200_1 (bvadd ((_ zero_extend 1) ?icost_8_0_200_1) ((_ zero_extend 1) ?bcost_8_0_200_1))))
(let ((?bcost_8_0_456_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_228) ((_ zero_extend 1) ?tcost_4_0_484))))
(let ((?icost_8_0_456_1 (bvadd ((_ zero_extend 1) ?icost_8_0_456) ((_ zero_extend 1) ?icost_8_4_456))))
(let ((?tcost_8_0_456_1 (bvadd ((_ zero_extend 1) ?icost_8_0_456_1) ((_ zero_extend 1) ?bcost_8_0_456_1))))
(let ((?bcost_16_0_400_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_200_1) ((_ zero_extend 1) ?tcost_8_0_456_1))))
(let ((?icost_16_0_400_1 (bvadd ((_ zero_extend 1) ?icost_16_0_400) ((_ zero_extend 1) ?icost_16_8_400))))
(let ((?icost_16_4_400_1 (bvadd ((_ zero_extend 1) ?icost_16_4_400) ((_ zero_extend 1) ?icost_16_12_400))))
(let ((?icost_16_0_400_2 (bvadd ((_ zero_extend 1) ?icost_16_0_400_1) ((_ zero_extend 1) ?icost_16_4_400_1))))
(let ((?tcost_16_0_400_2 (bvadd ((_ zero_extend 2) ?icost_16_0_400_2) ((_ zero_extend 1) ?bcost_16_0_400_2))))
(let ((?bcost_32_0_288_3 (bvadd ((_ zero_extend 1) ?tcost_16_0_144_2) ((_ zero_extend 1) ?tcost_16_0_400_2))))
(let ((?icost_32_0_288_1 (bvadd ((_ zero_extend 1) ?icost_32_0_288) ((_ zero_extend 1) ?icost_32_16_288))))
(let ((?icost_32_8_288_1 (bvadd ((_ zero_extend 1) ?icost_32_8_288) ((_ zero_extend 1) ?icost_32_24_288))))
(let ((?icost_32_0_288_2 (bvadd ((_ zero_extend 1) ?icost_32_0_288_1) ((_ zero_extend 1) ?icost_32_8_288_1))))
(let ((?icost_32_4_288_1 (bvadd ((_ zero_extend 1) ?icost_32_4_288) ((_ zero_extend 1) ?icost_32_20_288))))
(let ((?icost_32_12_288_1 (bvadd ((_ zero_extend 1) ?icost_32_12_288) ((_ zero_extend 1) ?icost_32_28_288))))
(let ((?icost_32_4_288_2 (bvadd ((_ zero_extend 1) ?icost_32_4_288_1) ((_ zero_extend 1) ?icost_32_12_288_1))))
(let ((?icost_32_0_288_3 (bvadd ((_ zero_extend 1) ?icost_32_0_288_2) ((_ zero_extend 1) ?icost_32_4_288_2))))
(let ((?tcost_32_0_288_3 (bvadd ((_ zero_extend 2) ?icost_32_0_288_3) ?bcost_32_0_288_3)))
(let ((?bcost_64_0_64_4 (bvadd ((_ zero_extend 1) ?tcost_32_0_32_3) ((_ zero_extend 1) ?tcost_32_0_288_3))))
(let ((?bmaxcost_64_0_64_4 (bvule ?bcost_64_0_64_4 (_ bv160 8))))
(let ((?icost_64_0_64_1 (bvadd ((_ zero_extend 1) ?icost_64_0_64) ((_ zero_extend 1) ?icost_64_32_64))))
(let ((?icost_64_16_64_1 (bvadd ((_ zero_extend 1) ?icost_64_16_64) ((_ zero_extend 1) ?icost_64_48_64))))
(let ((?icost_64_0_64_2 (bvadd ((_ zero_extend 1) ?icost_64_0_64_1) ((_ zero_extend 1) ?icost_64_16_64_1))))
(let ((?icost_64_8_64_1 (bvadd ((_ zero_extend 1) ?icost_64_8_64) ((_ zero_extend 1) ?icost_64_40_64))))
(let ((?icost_64_24_64_1 (bvadd ((_ zero_extend 1) ?icost_64_24_64) ((_ zero_extend 1) ?icost_64_56_64))))
(let ((?icost_64_8_64_2 (bvadd ((_ zero_extend 1) ?icost_64_8_64_1) ((_ zero_extend 1) ?icost_64_24_64_1))))
(let ((?icost_64_0_64_3 (bvadd ((_ zero_extend 1) ?icost_64_0_64_2) ((_ zero_extend 1) ?icost_64_8_64_2))))
(let ((?icost_64_4_64_1 (bvadd ((_ zero_extend 1) ?icost_64_4_64) ((_ zero_extend 1) ?icost_64_36_64))))
(let ((?icost_64_20_64_1 (bvadd ((_ zero_extend 1) ?icost_64_20_64) ((_ zero_extend 1) ?icost_64_52_64))))
(let ((?icost_64_4_64_2 (bvadd ((_ zero_extend 1) ?icost_64_4_64_1) ((_ zero_extend 1) ?icost_64_20_64_1))))
(let ((?icost_64_12_64_1 (bvadd ((_ zero_extend 1) ?icost_64_12_64) ((_ zero_extend 1) ?icost_64_44_64))))
(let ((?icost_64_28_64_1 (bvadd ((_ zero_extend 1) ?icost_64_28_64) ((_ zero_extend 1) ?icost_64_60_64))))
(let ((?icost_64_12_64_2 (bvadd ((_ zero_extend 1) ?icost_64_12_64_1) ((_ zero_extend 1) ?icost_64_28_64_1))))
(let ((?icost_64_4_64_3 (bvadd ((_ zero_extend 1) ?icost_64_4_64_2) ((_ zero_extend 1) ?icost_64_12_64_2))))
(let ((?icost_64_0_64_4 (bvadd ((_ zero_extend 1) ?icost_64_0_64_3) ((_ zero_extend 1) ?icost_64_4_64_3))))
(let ((?tcost_64_0_64_4 (bvadd ((_ zero_extend 2) ?icost_64_0_64_4) ?bcost_64_0_64_4)))
(let ((?tmaxcost_64_0_64_4 (bvule ?tcost_64_0_64_4 (_ bv160 8))))
(let ((?bcost_8_0_40_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_20) ((_ zero_extend 1) ?tcost_4_0_276))))
(let ((?icost_8_0_40_1 (bvadd ((_ zero_extend 1) ?icost_8_0_40) ((_ zero_extend 1) ?icost_8_4_40))))
(let ((?tcost_8_0_40_1 (bvadd ((_ zero_extend 1) ?icost_8_0_40_1) ((_ zero_extend 1) ?bcost_8_0_40_1))))
(let ((?bcost_8_0_296_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_148) ((_ zero_extend 1) ?tcost_4_0_404))))
(let ((?icost_8_0_296_1 (bvadd ((_ zero_extend 1) ?icost_8_0_296) ((_ zero_extend 1) ?icost_8_4_296))))
(let ((?tcost_8_0_296_1 (bvadd ((_ zero_extend 1) ?icost_8_0_296_1) ((_ zero_extend 1) ?bcost_8_0_296_1))))
(let ((?bcost_16_0_80_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_40_1) ((_ zero_extend 1) ?tcost_8_0_296_1))))
(let ((?icost_16_0_80_1 (bvadd ((_ zero_extend 1) ?icost_16_0_80) ((_ zero_extend 1) ?icost_16_8_80))))
(let ((?icost_16_4_80_1 (bvadd ((_ zero_extend 1) ?icost_16_4_80) ((_ zero_extend 1) ?icost_16_12_80))))
(let ((?icost_16_0_80_2 (bvadd ((_ zero_extend 1) ?icost_16_0_80_1) ((_ zero_extend 1) ?icost_16_4_80_1))))
(let ((?tcost_16_0_80_2 (bvadd ((_ zero_extend 2) ?icost_16_0_80_2) ((_ zero_extend 1) ?bcost_16_0_80_2))))
(let ((?bcost_8_0_168_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_84) ((_ zero_extend 1) ?tcost_4_0_340))))
(let ((?icost_8_0_168_1 (bvadd ((_ zero_extend 1) ?icost_8_0_168) ((_ zero_extend 1) ?icost_8_4_168))))
(let ((?tcost_8_0_168_1 (bvadd ((_ zero_extend 1) ?icost_8_0_168_1) ((_ zero_extend 1) ?bcost_8_0_168_1))))
(let ((?bcost_8_0_424_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_212) ((_ zero_extend 1) ?tcost_4_0_468))))
(let ((?icost_8_0_424_1 (bvadd ((_ zero_extend 1) ?icost_8_0_424) ((_ zero_extend 1) ?icost_8_4_424))))
(let ((?tcost_8_0_424_1 (bvadd ((_ zero_extend 1) ?icost_8_0_424_1) ((_ zero_extend 1) ?bcost_8_0_424_1))))
(let ((?bcost_16_0_336_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_168_1) ((_ zero_extend 1) ?tcost_8_0_424_1))))
(let ((?icost_16_0_336_1 (bvadd ((_ zero_extend 1) ?icost_16_0_336) ((_ zero_extend 1) ?icost_16_8_336))))
(let ((?icost_16_4_336_1 (bvadd ((_ zero_extend 1) ?icost_16_4_336) ((_ zero_extend 1) ?icost_16_12_336))))
(let ((?icost_16_0_336_2 (bvadd ((_ zero_extend 1) ?icost_16_0_336_1) ((_ zero_extend 1) ?icost_16_4_336_1))))
(let ((?tcost_16_0_336_2 (bvadd ((_ zero_extend 2) ?icost_16_0_336_2) ((_ zero_extend 1) ?bcost_16_0_336_2))))
(let ((?bcost_32_0_160_3 (bvadd ((_ zero_extend 1) ?tcost_16_0_80_2) ((_ zero_extend 1) ?tcost_16_0_336_2))))
(let ((?icost_32_0_160_1 (bvadd ((_ zero_extend 1) ?icost_32_0_160) ((_ zero_extend 1) ?icost_32_16_160))))
(let ((?icost_32_8_160_1 (bvadd ((_ zero_extend 1) ?icost_32_8_160) ((_ zero_extend 1) ?icost_32_24_160))))
(let ((?icost_32_0_160_2 (bvadd ((_ zero_extend 1) ?icost_32_0_160_1) ((_ zero_extend 1) ?icost_32_8_160_1))))
(let ((?icost_32_4_160_1 (bvadd ((_ zero_extend 1) ?icost_32_4_160) ((_ zero_extend 1) ?icost_32_20_160))))
(let ((?icost_32_12_160_1 (bvadd ((_ zero_extend 1) ?icost_32_12_160) ((_ zero_extend 1) ?icost_32_28_160))))
(let ((?icost_32_4_160_2 (bvadd ((_ zero_extend 1) ?icost_32_4_160_1) ((_ zero_extend 1) ?icost_32_12_160_1))))
(let ((?icost_32_0_160_3 (bvadd ((_ zero_extend 1) ?icost_32_0_160_2) ((_ zero_extend 1) ?icost_32_4_160_2))))
(let ((?tcost_32_0_160_3 (bvadd ((_ zero_extend 2) ?icost_32_0_160_3) ?bcost_32_0_160_3)))
(let ((?bcost_8_0_104_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_52) ((_ zero_extend 1) ?tcost_4_0_308))))
(let ((?icost_8_0_104_1 (bvadd ((_ zero_extend 1) ?icost_8_0_104) ((_ zero_extend 1) ?icost_8_4_104))))
(let ((?tcost_8_0_104_1 (bvadd ((_ zero_extend 1) ?icost_8_0_104_1) ((_ zero_extend 1) ?bcost_8_0_104_1))))
(let ((?bcost_8_0_360_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_180) ((_ zero_extend 1) ?tcost_4_0_436))))
(let ((?icost_8_0_360_1 (bvadd ((_ zero_extend 1) ?icost_8_0_360) ((_ zero_extend 1) ?icost_8_4_360))))
(let ((?tcost_8_0_360_1 (bvadd ((_ zero_extend 1) ?icost_8_0_360_1) ((_ zero_extend 1) ?bcost_8_0_360_1))))
(let ((?bcost_16_0_208_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_104_1) ((_ zero_extend 1) ?tcost_8_0_360_1))))
(let ((?icost_16_0_208_1 (bvadd ((_ zero_extend 1) ?icost_16_0_208) ((_ zero_extend 1) ?icost_16_8_208))))
(let ((?icost_16_4_208_1 (bvadd ((_ zero_extend 1) ?icost_16_4_208) ((_ zero_extend 1) ?icost_16_12_208))))
(let ((?icost_16_0_208_2 (bvadd ((_ zero_extend 1) ?icost_16_0_208_1) ((_ zero_extend 1) ?icost_16_4_208_1))))
(let ((?tcost_16_0_208_2 (bvadd ((_ zero_extend 2) ?icost_16_0_208_2) ((_ zero_extend 1) ?bcost_16_0_208_2))))
(let ((?bcost_8_0_232_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_116) ((_ zero_extend 1) ?tcost_4_0_372))))
(let ((?icost_8_0_232_1 (bvadd ((_ zero_extend 1) ?icost_8_0_232) ((_ zero_extend 1) ?icost_8_4_232))))
(let ((?tcost_8_0_232_1 (bvadd ((_ zero_extend 1) ?icost_8_0_232_1) ((_ zero_extend 1) ?bcost_8_0_232_1))))
(let ((?bcost_8_0_488_1 (bvadd ((_ zero_extend 1) ?tcost_4_0_244) ((_ zero_extend 1) ?tcost_4_0_500))))
(let ((?icost_8_0_488_1 (bvadd ((_ zero_extend 1) ?icost_8_0_488) ((_ zero_extend 1) ?icost_8_4_488))))
(let ((?tcost_8_0_488_1 (bvadd ((_ zero_extend 1) ?icost_8_0_488_1) ((_ zero_extend 1) ?bcost_8_0_488_1))))
(let ((?bcost_16_0_464_2 (bvadd ((_ zero_extend 1) ?tcost_8_0_232_1) ((_ zero_extend 1) ?tcost_8_0_488_1))))
(let ((?icost_16_0_464_1 (bvadd ((_ zero_extend 1) ?icost_16_0_464) ((_ zero_extend 1) ?icost_16_8_464))))
(let ((?icost_16_4_464_1 (bvadd ((_ zero_extend 1) ?icost_16_4_464) ((_ zero_extend 1) ?icost_16_12_464))))
(let ((?icost_16_0_464_2 (bvadd ((_ zero_extend 1) ?icost_16_0_464_1) ((_ zero_extend 1) ?icost_16_4_464_1))))
(let ((?tcost_16_0_464_2 (bvadd ((_ zero_extend 2) ?icost_16_0_464_2) ((_ zero_extend 1) ?bcost_16_0_464_2))))
(let ((?bcost_32_0_416_3 (bvadd ((_ zero_extend 1) ?tcost_16_0_208_2) ((_ zero_extend 1) ?tcost_16_0_464_2))))
(let ((?icost_32_0_416_1 (bvadd ((_ zero_extend 1) ?icost_32_0_416) ((_ zero_extend 1) ?icost_32_16_416))))
(let ((?icost_32_8_416_1 (bvadd ((_ zero_extend 1) ?icost_32_8_416) ((_ zero_extend 1) ?icost_32_24_416))))
(let ((?icost_32_0_416_2 (bvadd ((_ zero_extend 1) ?icost_32_0_416_1) ((_ zero_extend 1) ?icost_32_8_416_1))))
(let ((?icost_32_4_416_1 (bvadd ((_ zero_extend 1) ?icost_32_4_416) ((_ zero_extend 1) ?icost_32_20_416))))
(let ((?icost_32_12_416_1 (bvadd ((_ zero_extend 1) ?icost_32_12_416) ((_ zero_extend 1) ?icost_32_28_416))))
(let ((?icost_32_4_416_2 (bvadd ((_ zero_extend 1) ?icost_32_4_416_1) ((_ zero_extend 1) ?icost_32_12_416_1))))
(let ((?icost_32_0_416_3 (bvadd ((_ zero_extend 1) ?icost_32_0_416_2) ((_ zero_extend 1) ?icost_32_4_416_2))))
(let ((?tcost_32_0_416_3 (bvadd ((_ zero_extend 2) ?icost_32_0_416_3) ?bcost_32_0_416_3)))
(let ((?bcost_64_0_320_4 (bvadd ((_ zero_extend 1) ?tcost_32_0_160_3) ((_ zero_extend 1) ?tcost_32_0_416_3))))
(let ((?bmaxcost_64_0_320_4 (bvule ?bcost_64_0_320_4 (_ bv160 8))))
(let ((?icost_64_0_320_1 (bvadd ((_ zero_extend 1) ?icost_64_0_320) ((_ zero_extend 1) ?icost_64_32_320))))
(let ((?icost_64_16_320_1 (bvadd ((_ zero_extend 1) ?icost_64_16_320) ((_ zero_extend 1) ?icost_64_48_320))))
(let ((?icost_64_0_320_2 (bvadd ((_ zero_extend 1) ?icost_64_0_320_1) ((_ zero_extend 1) ?icost_64_16_320_1))))
(let ((?icost_64_8_320_1 (bvadd ((_ zero_extend 1) ?icost_64_8_320) ((_ zero_extend 1) ?icost_64_40_320))))
(let ((?icost_64_24_320_1 (bvadd ((_ zero_extend 1) ?icost_64_24_320) ((_ zero_extend 1) ?icost_64_56_320))))
(let ((?icost_64_8_320_2 (bvadd ((_ zero_extend 1) ?icost_64_8_320_1) ((_ zero_extend 1) ?icost_64_24_320_1))))
(let ((?icost_64_0_320_3 (bvadd ((_ zero_extend 1) ?icost_64_0_320_2) ((_ zero_extend 1) ?icost_64_8_320_2))))
(let ((?icost_64_4_320_1 (bvadd ((_ zero_extend 1) ?icost_64_4_320) ((_ zero_extend 1) ?icost_64_36_320))))
(let ((?icost_64_20_320_1 (bvadd ((_ zero_extend 1) ?icost_64_20_320) ((_ zero_extend 1) ?icost_64_52_320))))
(let ((?icost_64_4_320_2 (bvadd ((_ zero_extend 1) ?icost_64_4_320_1) ((_ zero_extend 1) ?icost_64_20_320_1))))
(let ((?icost_64_12_320_1 (bvadd ((_ zero_extend 1) ?icost_64_12_320) ((_ zero_extend 1) ?icost_64_44_320))))
(let ((?icost_64_28_320_1 (bvadd ((_ zero_extend 1) ?icost_64_28_320) ((_ zero_extend 1) ?icost_64_60_320))))
(let ((?icost_64_12_320_2 (bvadd ((_ zero_extend 1) ?icost_64_12_320_1) ((_ zero_extend 1) ?icost_64_28_320_1))))
(let ((?icost_64_4_320_3 (bvadd ((_ zero_extend 1) ?icost_64_4_320_2) ((_ zero_extend 1) ?icost_64_12_320_2))))
(let ((?icost_64_0_320_4 (bvadd ((_ zero_extend 1) ?icost_64_0_320_3) ((_ zero_extend 1) ?icost_64_4_320_3))))
(let ((?tcost_64_0_320_4 (bvadd ((_ zero_extend 2) ?icost_64_0_320_4) ?bcost_64_0_320_4)))
(let ((?tmaxcost_64_0_320_4 (bvule ?tcost_64_0_320_4 (_ bv160 8))))
(let ((?bcost_128_0_128_5 (bvadd ((_ zero_extend 1) ?tcost_64_0_64_4) ((_ zero_extend 1) ?tcost_64_0_320_4))))
(let ((?bmaxcost_128_0_128_5 (bvule ?bcost_128_0_128_5 (_ bv160 9))))
(let ((?icost_128_0_128_1 (bvadd ((_ zero_extend 1) ?icost_128_0_128) ((_ zero_extend 1) ?icost_128_64_128))))
(let ((?icost_128_32_128_1 (bvadd ((_ zero_extend 1) ?icost_128_32_128) ((_ zero_extend 1) ?icost_128_96_128))))
(let ((?icost_128_0_128_2 (bvadd ((_ zero_extend 1) ?icost_128_0_128_1) ((_ zero_extend 1) ?icost_128_32_128_1))))
(let ((?icost_128_16_128_1 (bvadd ((_ zero_extend 1) ?icost_128_16_128) ((_ zero_extend 1) ?icost_128_80_128))))
(let ((?icost_128_48_128_1 (bvadd ((_ zero_extend 1) ?icost_128_48_128) ((_ zero_extend 1) ?icost_128_112_128))))
(let ((?icost_128_16_128_2 (bvadd ((_ zero_extend 1) ?icost_128_16_128_1) ((_ zero_extend 1) ?icost_128_48_128_1))))
(let ((?icost_128_0_128_3 (bvadd ((_ zero_extend 1) ?icost_128_0_128_2) ((_ zero_extend 1) ?icost_128_16_128_2))))
(let ((?icost_128_8_128_1 (bvadd ((_ zero_extend 1) ?icost_128_8_128) ((_ zero_extend 1) ?icost_128_72_128))))
(let ((?icost_128_40_128_1 (bvadd ((_ zero_extend 1) ?icost_128_40_128) ((_ zero_extend 1) ?icost_128_104_128))))
(let ((?icost_128_8_128_2 (bvadd ((_ zero_extend 1) ?icost_128_8_128_1) ((_ zero_extend 1) ?icost_128_40_128_1))))
(let ((?icost_128_24_128_1 (bvadd ((_ zero_extend 1) ?icost_128_24_128) ((_ zero_extend 1) ?icost_128_88_128))))
(let ((?icost_128_56_128_1 (bvadd ((_ zero_extend 1) ?icost_128_56_128) ((_ zero_extend 1) ?icost_128_120_128))))
(let ((?icost_128_24_128_2 (bvadd ((_ zero_extend 1) ?icost_128_24_128_1) ((_ zero_extend 1) ?icost_128_56_128_1))))
(let ((?icost_128_8_128_3 (bvadd ((_ zero_extend 1) ?icost_128_8_128_2) ((_ zero_extend 1) ?icost_128_24_128_2))))
(let ((?icost_128_0_128_4 (bvadd ((_ zero_extend 1) ?icost_128_0_128_3) ((_ zero_extend 1) ?icost_128_8_128_3))))
(let ((?icost_128_4_128_1 (bvadd ((_ zero_extend 1) ?icost_128_4_128) ((_ zero_extend 1) ?icost_128_68_128))))
(let ((?icost_128_36_128_1 (bvadd ((_ zero_extend 1) ?icost_128_36_128) ((_ zero_extend 1) ?icost_128_100_128))))
(let ((?icost_128_4_128_2 (bvadd ((_ zero_extend 1) ?icost_128_4_128_1) ((_ zero_extend 1) ?icost_128_36_128_1))))
(let ((?icost_128_20_128_1 (bvadd ((_ zero_extend 1) ?icost_128_20_128) ((_ zero_extend 1) ?icost_128_84_128))))
(let ((?icost_128_52_128_1 (bvadd ((_ zero_extend 1) ?icost_128_52_128) ((_ zero_extend 1) ?icost_128_116_128))))
(let ((?icost_128_20_128_2 (bvadd ((_ zero_extend 1) ?icost_128_20_128_1) ((_ zero_extend 1) ?icost_128_52_128_1))))
(let ((?icost_128_4_128_3 (bvadd ((_ zero_extend 1) ?icost_128_4_128_2) ((_ zero_extend 1) ?icost_128_20_128_2))))
(let ((?icost_128_12_128_1 (bvadd ((_ zero_extend 1) ?icost_128_12_128) ((_ zero_extend 1) ?icost_128_76_128))))
(let ((?icost_128_44_128_1 (bvadd ((_ zero_extend 1) ?icost_128_44_128) ((_ zero_extend 1) ?icost_128_108_128))))
(let ((?icost_128_12_128_2 (bvadd ((_ zero_extend 1) ?icost_128_12_128_1) ((_ zero_extend 1) ?icost_128_44_128_1))))
(let ((?icost_128_28_128_1 (bvadd ((_ zero_extend 1) ?icost_128_28_128) ((_ zero_extend 1) ?icost_128_92_128))))
(let ((?icost_128_60_128_1 (bvadd ((_ zero_extend 1) ?icost_128_60_128) ((_ zero_extend 1) ?icost_128_124_128))))
(let ((?icost_128_28_128_2 (bvadd ((_ zero_extend 1) ?icost_128_28_128_1) ((_ zero_extend 1) ?icost_128_60_128_1))))
(let ((?icost_128_12_128_3 (bvadd ((_ zero_extend 1) ?icost_128_12_128_2) ((_ zero_extend 1) ?icost_128_28_128_2))))
(let ((?icost_128_4_128_4 (bvadd ((_ zero_extend 1) ?icost_128_4_128_3) ((_ zero_extend 1) ?icost_128_12_128_3))))
(let ((?icost_128_0_128_5 (bvadd ((_ zero_extend 1) ?icost_128_0_128_4) ((_ zero_extend 1) ?icost_128_4_128_4))))
(let ((?tcost_128_0_128_5 (bvadd ((_ zero_extend 2) ?icost_128_0_128_5) ?bcost_128_0_128_5)))
(let ((?tmaxcost_128_0_128_5 (bvule ?tcost_128_0_128_5 (_ bv160 9))))
(let ((?good (and true ?bmaxcost_64_0_64_4 ?tmaxcost_64_0_64_4 ?bmaxcost_64_0_320_4 ?tmaxcost_64_0_320_4 ?bmaxcost_128_0_128_5 ?tmaxcost_128_0_128_5
)))
(let ((?bad (or false ?pinzero_128_0_128_1 ?pinzero_128_4_128_1 ?pinzero_128_8_128_1 ?pinzero_128_12_128_1 ?pinzero_128_16_128_1 ?pinzero_128_20_128_1
 ?pinzero_128_24_128_1 ?pinzero_128_28_128_1 ?pinzero_128_32_128_1 ?pinzero_128_36_128_1 ?pinzero_128_40_128_1 ?pinzero_128_44_128_1
 ?pinzero_128_48_128_1 ?pinzero_128_52_128_1 ?pinzero_128_56_128_1 ?pinzero_128_60_128_1 ?pinzero_64_0_64_1 ?pinzero_64_4_64_1
 ?pinzero_64_8_64_1 ?pinzero_64_12_64_1 ?pinzero_64_16_64_1 ?pinzero_64_20_64_1 ?pinzero_64_24_64_1 ?pinzero_64_28_64_1
 ?pinzero_64_0_320_1 ?pinzero_64_4_320_1 ?pinzero_64_8_320_1 ?pinzero_64_12_320_1 ?pinzero_64_16_320_1 ?pinzero_64_20_320_1
 ?pinzero_64_24_320_1 ?pinzero_64_28_320_1 ?pinzero_32_0_32_1 ?pinzero_32_4_32_1 ?pinzero_32_8_32_1 ?pinzero_32_12_32_1
 ?pinzero_32_0_288_1 ?pinzero_32_4_288_1 ?pinzero_32_8_288_1 ?pinzero_32_12_288_1 ?pinzero_32_0_160_1 ?pinzero_32_4_160_1
 ?pinzero_32_8_160_1 ?pinzero_32_12_160_1 ?pinzero_32_0_416_1 ?pinzero_32_4_416_1 ?pinzero_32_8_416_1 ?pinzero_32_12_416_1
 ?pinzero_16_0_16_1 ?pinzero_16_4_16_1 ?pinzero_16_0_272_1 ?pinzero_16_4_272_1 ?pinzero_16_0_144_1 ?pinzero_16_4_144_1
 ?pinzero_16_0_400_1 ?pinzero_16_4_400_1 ?pinzero_16_0_80_1 ?pinzero_16_4_80_1 ?pinzero_16_0_336_1 ?pinzero_16_4_336_1
 ?pinzero_16_0_208_1 ?pinzero_16_4_208_1 ?pinzero_16_0_464_1 ?pinzero_16_4_464_1 ?pinzero_8_0_8_1 ?pinzero_8_0_264_1
 ?pinzero_8_0_136_1 ?pinzero_8_0_392_1 ?pinzero_8_0_72_1 ?pinzero_8_0_328_1 ?pinzero_8_0_200_1 ?pinzero_8_0_456_1
 ?pinzero_8_0_40_1 ?pinzero_8_0_296_1 ?pinzero_8_0_168_1 ?pinzero_8_0_424_1 ?pinzero_8_0_104_1 ?pinzero_8_0_360_1
 ?pinzero_8_0_232_1 ?pinzero_8_0_488_1 ?pushup_128_0_128_1 ?pushup_128_4_128_1 ?pushup_128_8_128_1 ?pushup_128_12_128_1
 ?pushup_128_16_128_1 ?pushup_128_20_128_1 ?pushup_128_24_128_1 ?pushup_128_28_128_1 ?pushup_128_32_128_1 ?pushup_128_36_128_1
 ?pushup_128_40_128_1 ?pushup_128_44_128_1 ?pushup_128_48_128_1 ?pushup_128_52_128_1 ?pushup_128_56_128_1 ?pushup_128_60_128_1
 ?pushup_64_0_64_1 ?pushup_64_4_64_1 ?pushup_64_8_64_1 ?pushup_64_12_64_1 ?pushup_64_16_64_1 ?pushup_64_20_64_1
 ?pushup_64_24_64_1 ?pushup_64_28_64_1 ?pushup_64_0_320_1 ?pushup_64_4_320_1 ?pushup_64_8_320_1 ?pushup_64_12_320_1
 ?pushup_64_16_320_1 ?pushup_64_20_320_1 ?pushup_64_24_320_1 ?pushup_64_28_320_1 ?pushup_32_0_32_1 ?pushup_32_4_32_1
 ?pushup_32_8_32_1 ?pushup_32_12_32_1 ?pushup_32_0_288_1 ?pushup_32_4_288_1 ?pushup_32_8_288_1 ?pushup_32_12_288_1
 ?pushup_32_0_160_1 ?pushup_32_4_160_1 ?pushup_32_8_160_1 ?pushup_32_12_160_1 ?pushup_32_0_416_1 ?pushup_32_4_416_1
 ?pushup_32_8_416_1 ?pushup_32_12_416_1 ?pushup_16_0_16_1 ?pushup_16_4_16_1 ?pushup_16_0_272_1 ?pushup_16_4_272_1
 ?pushup_16_0_144_1 ?pushup_16_4_144_1 ?pushup_16_0_400_1 ?pushup_16_4_400_1 ?pushup_16_0_80_1 ?pushup_16_4_80_1
 ?pushup_16_0_336_1 ?pushup_16_4_336_1 ?pushup_16_0_208_1 ?pushup_16_4_208_1 ?pushup_16_0_464_1 ?pushup_16_4_464_1
 ?pushup_8_0_8_1 ?pushup_8_0_264_1 ?pushup_8_0_136_1 ?pushup_8_0_392_1 ?pushup_8_0_72_1 ?pushup_8_0_328_1
 ?pushup_8_0_200_1 ?pushup_8_0_456_1 ?pushup_8_0_40_1 ?pushup_8_0_296_1 ?pushup_8_0_168_1 ?pushup_8_0_424_1
 ?pushup_8_0_104_1 ?pushup_8_0_360_1 ?pushup_8_0_232_1 ?pushup_8_0_488_1)))
(and ?good (not ?bad)))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
))))))))))))))))))))))))))))))
)))))))
(check-sat)
(exit)
